:: by Janusz Ganczarski

::

:: Received May 23, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

theorem Th1: :: LATSUBGR:1

for G being Group

for H1, H2 being Subgroup of G holds the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2

for H1, H2 being Subgroup of G holds the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2

proof end;

theorem Th2: :: LATSUBGR:2

for G being Group

for h being set holds

( h in Subgroups G iff ex H being strict Subgroup of G st h = H )

for h being set holds

( h in Subgroups G iff ex H being strict Subgroup of G st h = H )

proof end;

theorem Th3: :: LATSUBGR:3

for G being Group

for A being Subset of G

for H being strict Subgroup of G st A = the carrier of H holds

gr A = H

for A being Subset of G

for H being strict Subgroup of G st A = the carrier of H holds

gr A = H

proof end;

theorem Th4: :: LATSUBGR:4

for G being Group

for H1, H2 being Subgroup of G

for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds

H1 "\/" H2 = gr A

for H1, H2 being Subgroup of G

for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds

H1 "\/" H2 = gr A

proof end;

theorem Th5: :: LATSUBGR:5

for G being Group

for H1, H2 being Subgroup of G

for g being Element of G st ( g in H1 or g in H2 ) holds

g in H1 "\/" H2

for H1, H2 being Subgroup of G

for g being Element of G st ( g in H1 or g in H2 ) holds

g in H1 "\/" H2

proof end;

theorem :: LATSUBGR:6

for G1, G2 being Group

for f being Homomorphism of G1,G2

for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1

for f being Homomorphism of G1,G2

for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1

proof end;

theorem :: LATSUBGR:7

for G1, G2 being Group

for f being Homomorphism of G1,G2

for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2

for f being Homomorphism of G1,G2

for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2

proof end;

theorem :: LATSUBGR:8

for G1, G2 being Group

for f being Homomorphism of G1,G2

for H1, H2 being Subgroup of G1

for H3, H4 being Subgroup of G2 st the carrier of H3 = f .: the carrier of H1 & the carrier of H4 = f .: the carrier of H2 & H1 is Subgroup of H2 holds

H3 is Subgroup of H4

for f being Homomorphism of G1,G2

for H1, H2 being Subgroup of G1

for H3, H4 being Subgroup of G2 st the carrier of H3 = f .: the carrier of H1 & the carrier of H4 = f .: the carrier of H2 & H1 is Subgroup of H2 holds

H3 is Subgroup of H4

proof end;

theorem :: LATSUBGR:9

for G1, G2 being Group

for f being Homomorphism of G1,G2

for H1, H2 being Subgroup of G2

for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds

H3 is Subgroup of H4

for f being Homomorphism of G1,G2

for H1, H2 being Subgroup of G2

for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds

H3 is Subgroup of H4

proof end;

theorem :: LATSUBGR:10

for G1, G2 being Group

for f being Function of the carrier of G1, the carrier of G2

for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)

for f being Function of the carrier of G1, the carrier of G2

for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A)

proof end;

theorem :: LATSUBGR:11

definition

let G be Group;

ex b_{1} being Function of (Subgroups G),(bool the carrier of G) st

for H being strict Subgroup of G holds b_{1} . H = the carrier of H

for b_{1}, b_{2} being Function of (Subgroups G),(bool the carrier of G) st ( for H being strict Subgroup of G holds b_{1} . H = the carrier of H ) & ( for H being strict Subgroup of G holds b_{2} . H = the carrier of H ) holds

b_{1} = b_{2}

end;
func carr G -> Function of (Subgroups G),(bool the carrier of G) means :Def1: :: LATSUBGR:def 1

for H being strict Subgroup of G holds it . H = the carrier of H;

existence for H being strict Subgroup of G holds it . H = the carrier of H;

ex b

for H being strict Subgroup of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines carr LATSUBGR:def 1 :

for G being Group

for b_{2} being Function of (Subgroups G),(bool the carrier of G) holds

( b_{2} = carr G iff for H being strict Subgroup of G holds b_{2} . H = the carrier of H );

for G being Group

for b

( b

theorem Th13: :: LATSUBGR:13

for G being Group

for H being strict Subgroup of G

for x being Element of G holds

( x in (carr G) . H iff x in H )

for H being strict Subgroup of G

for x being Element of G holds

( x in (carr G) . H iff x in H )

proof end;

theorem :: LATSUBGR:15

theorem :: LATSUBGR:16

for G being Group

for H being strict Subgroup of G

for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds

g1 * g2 in (carr G) . H

for H being strict Subgroup of G

for g1, g2 being Element of G st g1 in (carr G) . H & g2 in (carr G) . H holds

g1 * g2 in (carr G) . H

proof end;

theorem :: LATSUBGR:17

for G being Group

for H being strict Subgroup of G

for g being Element of G st g in (carr G) . H holds

g " in (carr G) . H

for H being strict Subgroup of G

for g being Element of G st g in (carr G) . H holds

g " in (carr G) . H

proof end;

theorem Th18: :: LATSUBGR:18

for G being Group

for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)

for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)

proof end;

theorem :: LATSUBGR:19

for G being Group

for H1, H2 being strict Subgroup of G holds (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)

for H1, H2 being strict Subgroup of G holds (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2)

proof end;

definition

let G be Group;

let F be non empty Subset of (Subgroups G);

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = meet ((carr G) .: F)

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = meet ((carr G) .: F) & the carrier of b_{2} = meet ((carr G) .: F) holds

b_{1} = b_{2}
by GROUP_2:59;

end;
let F be non empty Subset of (Subgroups G);

func meet F -> strict Subgroup of G means :Def2: :: LATSUBGR:def 2

the carrier of it = meet ((carr G) .: F);

existence the carrier of it = meet ((carr G) .: F);

ex b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines meet LATSUBGR:def 2 :

for G being Group

for F being non empty Subset of (Subgroups G)

for b_{3} being strict Subgroup of G holds

( b_{3} = meet F iff the carrier of b_{3} = meet ((carr G) .: F) );

for G being Group

for F being non empty Subset of (Subgroups G)

for b

( b

theorem :: LATSUBGR:20

for G being Group

for F being non empty Subset of (Subgroups G) st (1). G in F holds

meet F = (1). G

for F being non empty Subset of (Subgroups G) st (1). G in F holds

meet F = (1). G

proof end;

theorem :: LATSUBGR:21

for G being Group

for h being Element of Subgroups G

for F being non empty Subset of (Subgroups G) st F = {h} holds

meet F = h

for h being Element of Subgroups G

for F being non empty Subset of (Subgroups G) st F = {h} holds

meet F = h

proof end;

theorem Th22: :: LATSUBGR:22

for G being Group

for H1, H2 being Subgroup of G

for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds

h1 "\/" h2 = H1 "\/" H2

for H1, H2 being Subgroup of G

for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds

h1 "\/" h2 = H1 "\/" H2

proof end;

theorem Th23: :: LATSUBGR:23

for G being Group

for H1, H2 being Subgroup of G

for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds

h1 "/\" h2 = H1 /\ H2

for H1, H2 being Subgroup of G

for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds

h1 "/\" h2 = H1 /\ H2

proof end;

theorem :: LATSUBGR:24

theorem Th25: :: LATSUBGR:25

for G being Group

for H1, H2 being Subgroup of G

for p, q being Element of (lattice G) st p = H1 & q = H2 holds

( p [= q iff the carrier of H1 c= the carrier of H2 )

for H1, H2 being Subgroup of G

for p, q being Element of (lattice G) st p = H1 & q = H2 holds

( p [= q iff the carrier of H1 c= the carrier of H2 )

proof end;

theorem :: LATSUBGR:26

for G being Group

for H1, H2 being Subgroup of G

for p, q being Element of (lattice G) st p = H1 & q = H2 holds

( p [= q iff H1 is Subgroup of H2 )

for H1, H2 being Subgroup of G

for p, q being Element of (lattice G) st p = H1 & q = H2 holds

( p [= q iff H1 is Subgroup of H2 )

proof end;

definition

let G1, G2 be Group;

let f be Function of the carrier of G1, the carrier of G2;

ex b_{1} being Function of the carrier of (lattice G1), the carrier of (lattice G2) st

for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

b_{1} . H = gr A

for b_{1}, b_{2} being Function of the carrier of (lattice G1), the carrier of (lattice G2) st ( for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

b_{1} . H = gr A ) & ( for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

b_{2} . H = gr A ) holds

b_{1} = b_{2}

end;
let f be Function of the carrier of G1, the carrier of G2;

func FuncLatt f -> Function of the carrier of (lattice G1), the carrier of (lattice G2) means :Def3: :: LATSUBGR:def 3

for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

it . H = gr A;

existence for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

it . H = gr A;

ex b

for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

b

proof end;

uniqueness for b

for A being Subset of G2 st A = f .: the carrier of H holds

b

for A being Subset of G2 st A = f .: the carrier of H holds

b

b

proof end;

:: deftheorem Def3 defines FuncLatt LATSUBGR:def 3 :

for G1, G2 being Group

for f being Function of the carrier of G1, the carrier of G2

for b_{4} being Function of the carrier of (lattice G1), the carrier of (lattice G2) holds

( b_{4} = FuncLatt f iff for H being strict Subgroup of G1

for A being Subset of G2 st A = f .: the carrier of H holds

b_{4} . H = gr A );

for G1, G2 being Group

for f being Function of the carrier of G1, the carrier of G2

for b

( b

for A being Subset of G2 st A = f .: the carrier of H holds

b

theorem :: LATSUBGR:29

for G1, G2 being Group

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is one-to-one

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is one-to-one

proof end;

theorem Th31: :: LATSUBGR:31

for G1, G2 being Group

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2)

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2)

proof end;

theorem Th32: :: LATSUBGR:32

for G1, G2 being Group

for f being Homomorphism of G1,G2 holds FuncLatt f is sup-Semilattice-Homomorphism of (lattice G1),(lattice G2)

for f being Homomorphism of G1,G2 holds FuncLatt f is sup-Semilattice-Homomorphism of (lattice G1),(lattice G2)

proof end;

theorem :: LATSUBGR:33

for G1, G2 being Group

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is Homomorphism of (lattice G1),(lattice G2) by Th31, Th32;

for f being Homomorphism of G1,G2 st f is one-to-one holds

FuncLatt f is Homomorphism of (lattice G1),(lattice G2) by Th31, Th32;