:: LATSUBGR semantic presentation begin 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 proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 let H1, H2 be Subgroup of G; ::_thesis: the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 the carrier of H2 = carr H2 by GROUP_2:def_9; then the carrier of H1 /\ the carrier of H2 = (carr H1) /\ (carr H2) by GROUP_2:def_9; hence the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by GROUP_2:def_10; ::_thesis: verum 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 ) proof let G be Group; ::_thesis: for h being set holds ( h in Subgroups G iff ex H being strict Subgroup of G st h = H ) let h be set ; ::_thesis: ( h in Subgroups G iff ex H being strict Subgroup of G st h = H ) thus ( h in Subgroups G implies ex H being strict Subgroup of G st h = H ) ::_thesis: ( ex H being strict Subgroup of G st h = H implies h in Subgroups G ) proof assume h in Subgroups G ; ::_thesis: ex H being strict Subgroup of G st h = H then h is strict Subgroup of G by GROUP_3:def_1; hence ex H being strict Subgroup of G st h = H ; ::_thesis: verum end; thus ( ex H being strict Subgroup of G st h = H implies h in Subgroups G ) by GROUP_3:def_1; ::_thesis: verum 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 proof let G be Group; ::_thesis: for A being Subset of G for H being strict Subgroup of G st A = the carrier of H holds gr A = H let A be Subset of G; ::_thesis: for H being strict Subgroup of G st A = the carrier of H holds gr A = H let H be strict Subgroup of G; ::_thesis: ( A = the carrier of H implies gr A = H ) assume A1: A = the carrier of H ; ::_thesis: gr A = H gr (carr H) = H by GROUP_4:31; hence gr A = H by A1, GROUP_2:def_9; ::_thesis: verum 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 proof let G be Group; ::_thesis: 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 let H1, H2 be Subgroup of G; ::_thesis: for A being Subset of G st A = the carrier of H1 \/ the carrier of H2 holds H1 "\/" H2 = gr A A1: the carrier of H2 = carr H2 by GROUP_2:def_9; let A be Subset of G; ::_thesis: ( A = the carrier of H1 \/ the carrier of H2 implies H1 "\/" H2 = gr A ) assume A = the carrier of H1 \/ the carrier of H2 ; ::_thesis: H1 "\/" H2 = gr A hence H1 "\/" H2 = gr A by A1, GROUP_2:def_9; ::_thesis: verum 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 proof let G be Group; ::_thesis: 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 let H1, H2 be Subgroup of G; ::_thesis: for g being Element of G st ( g in H1 or g in H2 ) holds g in H1 "\/" H2 let g be Element of G; ::_thesis: ( ( g in H1 or g in H2 ) implies g in H1 "\/" H2 ) assume A1: ( g in H1 or g in H2 ) ; ::_thesis: g in H1 "\/" H2 now__::_thesis:_g_in_H1_"\/"_H2 percases ( g in H1 or g in H2 ) by A1; supposeA2: g in H1 ; ::_thesis: g in H1 "\/" H2 ( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by GROUP_2:def_5; then reconsider A = the carrier of H1 \/ the carrier of H2 as Subset of G by XBOOLE_1:8; g in the carrier of H1 by A2, STRUCT_0:def_5; then g in A by XBOOLE_0:def_3; then g in gr A by GROUP_4:29; hence g in H1 "\/" H2 by Th4; ::_thesis: verum end; supposeA3: g in H2 ; ::_thesis: g in H1 "\/" H2 ( the carrier of H1 c= the carrier of G & the carrier of H2 c= the carrier of G ) by GROUP_2:def_5; then reconsider A = the carrier of H1 \/ the carrier of H2 as Subset of G by XBOOLE_1:8; g in the carrier of H2 by A3, STRUCT_0:def_5; then g in A by XBOOLE_0:def_3; then g in gr A by GROUP_4:29; hence g in H1 "\/" H2 by Th4; ::_thesis: verum end; end; end; hence g in H1 "\/" H2 ; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: 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 let f be Homomorphism of G1,G2; ::_thesis: for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1 let H1 be Subgroup of G1; ::_thesis: ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1 reconsider y = f . (1_ G1) as Element of G2 ; A1: for g being Element of G2 st g in f .: the carrier of H1 holds g " in f .: the carrier of H1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of H1 implies g " in f .: the carrier of H1 ) assume g in f .: the carrier of H1 ; ::_thesis: g " in f .: the carrier of H1 then consider x being Element of G1 such that A2: x in the carrier of H1 and A3: g = f . x by FUNCT_2:65; x in H1 by A2, STRUCT_0:def_5; then x " in H1 by GROUP_2:51; then A4: x " in the carrier of H1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of H1 by A3, A4, FUNCT_2:35; ::_thesis: verum end; A5: for g1, g2 being Element of G2 st g1 in f .: the carrier of H1 & g2 in f .: the carrier of H1 holds g1 * g2 in f .: the carrier of H1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of H1 & g2 in f .: the carrier of H1 implies g1 * g2 in f .: the carrier of H1 ) assume that A6: g1 in f .: the carrier of H1 and A7: g2 in f .: the carrier of H1 ; ::_thesis: g1 * g2 in f .: the carrier of H1 consider x being Element of G1 such that A8: x in the carrier of H1 and A9: g1 = f . x by A6, FUNCT_2:65; consider y being Element of G1 such that A10: y in the carrier of H1 and A11: g2 = f . y by A7, FUNCT_2:65; A12: y in H1 by A10, STRUCT_0:def_5; x in H1 by A8, STRUCT_0:def_5; then x * y in H1 by A12, GROUP_2:50; then A13: x * y in the carrier of H1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of H1 by A9, A11, A13, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in H1 by GROUP_2:46; then ( dom f = the carrier of G1 & 1_ G1 in the carrier of H1 ) by FUNCT_2:def_1, STRUCT_0:def_5; then y in f .: the carrier of H1 by FUNCT_1:def_6; then consider H2 being strict Subgroup of G2 such that A14: the carrier of H2 = f .: the carrier of H1 by A1, A5, GROUP_2:52; take H2 ; ::_thesis: the carrier of H2 = f .: the carrier of H1 thus the carrier of H2 = f .: the carrier of H1 by A14; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: 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 let f be Homomorphism of G1,G2; ::_thesis: for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2 let H2 be Subgroup of G2; ::_thesis: ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2 A1: for g being Element of G1 st g in f " the carrier of H2 holds g " in f " the carrier of H2 proof let g be Element of G1; ::_thesis: ( g in f " the carrier of H2 implies g " in f " the carrier of H2 ) assume g in f " the carrier of H2 ; ::_thesis: g " in f " the carrier of H2 then f . g in the carrier of H2 by FUNCT_2:38; then f . g in H2 by STRUCT_0:def_5; then (f . g) " in H2 by GROUP_2:51; then f . (g ") in H2 by GROUP_6:32; then f . (g ") in the carrier of H2 by STRUCT_0:def_5; hence g " in f " the carrier of H2 by FUNCT_2:38; ::_thesis: verum end; A2: for g1, g2 being Element of G1 st g1 in f " the carrier of H2 & g2 in f " the carrier of H2 holds g1 * g2 in f " the carrier of H2 proof let g1, g2 be Element of G1; ::_thesis: ( g1 in f " the carrier of H2 & g2 in f " the carrier of H2 implies g1 * g2 in f " the carrier of H2 ) assume that A3: g1 in f " the carrier of H2 and A4: g2 in f " the carrier of H2 ; ::_thesis: g1 * g2 in f " the carrier of H2 f . g2 in the carrier of H2 by A4, FUNCT_2:38; then A5: f . g2 in H2 by STRUCT_0:def_5; f . g1 in the carrier of H2 by A3, FUNCT_2:38; then f . g1 in H2 by STRUCT_0:def_5; then (f . g1) * (f . g2) in H2 by A5, GROUP_2:50; then f . (g1 * g2) in H2 by GROUP_6:def_6; then f . (g1 * g2) in the carrier of H2 by STRUCT_0:def_5; hence g1 * g2 in f " the carrier of H2 by FUNCT_2:38; ::_thesis: verum end; 1_ G2 in H2 by GROUP_2:46; then 1_ G2 in the carrier of H2 by STRUCT_0:def_5; then f . (1_ G1) in the carrier of H2 by GROUP_6:31; then f " the carrier of H2 <> {} by FUNCT_2:38; then consider H1 being strict Subgroup of G1 such that A6: the carrier of H1 = f " the carrier of H2 by A1, A2, GROUP_2:52; take H1 ; ::_thesis: the carrier of H1 = f " the carrier of H2 thus the carrier of H1 = f " the carrier of H2 by A6; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: 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 let f be Homomorphism of G1,G2; ::_thesis: 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 let H1, H2 be Subgroup of G1; ::_thesis: 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 let H3, H4 be Subgroup of G2; ::_thesis: ( the carrier of H3 = f .: the carrier of H1 & the carrier of H4 = f .: the carrier of H2 & H1 is Subgroup of H2 implies H3 is Subgroup of H4 ) assume A1: ( the carrier of H3 = f .: the carrier of H1 & the carrier of H4 = f .: the carrier of H2 ) ; ::_thesis: ( not H1 is Subgroup of H2 or H3 is Subgroup of H4 ) assume H1 is Subgroup of H2 ; ::_thesis: H3 is Subgroup of H4 then the carrier of H1 c= the carrier of H2 by GROUP_2:def_5; hence H3 is Subgroup of H4 by A1, GROUP_2:57, RELAT_1:123; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: 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 let f be Homomorphism of G1,G2; ::_thesis: 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 let H1, H2 be Subgroup of G2; ::_thesis: 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 let H3, H4 be Subgroup of G1; ::_thesis: ( the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 implies H3 is Subgroup of H4 ) assume A1: ( the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 ) ; ::_thesis: ( not H1 is Subgroup of H2 or H3 is Subgroup of H4 ) assume H1 is Subgroup of H2 ; ::_thesis: H3 is Subgroup of H4 then the carrier of H1 c= the carrier of H2 by GROUP_2:def_5; hence H3 is Subgroup of H4 by A1, GROUP_2:57, RELAT_1:143; ::_thesis: verum 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) proof let G1, G2 be Group; ::_thesis: 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) let f be Function of the carrier of G1, the carrier of G2; ::_thesis: for A being Subset of G1 holds f .: A c= f .: the carrier of (gr A) let A be Subset of G1; ::_thesis: f .: A c= f .: the carrier of (gr A) A c= the carrier of (gr A) by GROUP_4:def_4; hence f .: A c= f .: the carrier of (gr A) by RELAT_1:123; ::_thesis: verum end; theorem :: LATSUBGR:11 for G1, G2 being Group for H1, H2 being Subgroup of G1 for f being Function of the carrier of G1, the carrier of G2 for A being Subset of G1 st A = the carrier of H1 \/ the carrier of H2 holds f .: the carrier of (H1 "\/" H2) = f .: the carrier of (gr A) by Th4; theorem Th12: :: LATSUBGR:12 for G being Group for A being Subset of G st A = {(1_ G)} holds gr A = (1). G proof let G be Group; ::_thesis: for A being Subset of G st A = {(1_ G)} holds gr A = (1). G let A be Subset of G; ::_thesis: ( A = {(1_ G)} implies gr A = (1). G ) assume A = {(1_ G)} ; ::_thesis: gr A = (1). G then A = the carrier of ((1). G) by GROUP_2:def_7; hence gr A = (1). G by Th3; ::_thesis: verum end; definition let G be Group; 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 ex b1 being Function of (Subgroups G),(bool the carrier of G) st for H being strict Subgroup of G holds b1 . H = the carrier of H proof defpred S1[ set , set ] means for h being strict Subgroup of G st h = \$1 holds \$2 = the carrier of h; A1: for e being set st e in Subgroups G holds ex u being set st ( u in bool the carrier of G & S1[e,u] ) proof let e be set ; ::_thesis: ( e in Subgroups G implies ex u being set st ( u in bool the carrier of G & S1[e,u] ) ) assume e in Subgroups G ; ::_thesis: ex u being set st ( u in bool the carrier of G & S1[e,u] ) then reconsider E = e as strict Subgroup of G by GROUP_3:def_1; reconsider u = carr E as Subset of G ; take u ; ::_thesis: ( u in bool the carrier of G & S1[e,u] ) thus ( u in bool the carrier of G & S1[e,u] ) by GROUP_2:def_9; ::_thesis: verum end; consider f being Function of (Subgroups G),(bool the carrier of G) such that A2: for e being set st e in Subgroups G holds S1[e,f . e] from FUNCT_2:sch_1(A1); take f ; ::_thesis: for H being strict Subgroup of G holds f . H = the carrier of H let H be strict Subgroup of G; ::_thesis: f . H = the carrier of H H in Subgroups G by GROUP_3:def_1; hence f . H = the carrier of H by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of (Subgroups G),(bool the carrier of G) st ( for H being strict Subgroup of G holds b1 . H = the carrier of H ) & ( for H being strict Subgroup of G holds b2 . H = the carrier of H ) holds b1 = b2 proof let F1, F2 be Function of (Subgroups G),(bool the carrier of G); ::_thesis: ( ( for H being strict Subgroup of G holds F1 . H = the carrier of H ) & ( for H being strict Subgroup of G holds F2 . H = the carrier of H ) implies F1 = F2 ) assume that A3: for H1 being strict Subgroup of G holds F1 . H1 = the carrier of H1 and A4: for H2 being strict Subgroup of G holds F2 . H2 = the carrier of H2 ; ::_thesis: F1 = F2 for h being set st h in Subgroups G holds F1 . h = F2 . h proof let h be set ; ::_thesis: ( h in Subgroups G implies F1 . h = F2 . h ) assume h in Subgroups G ; ::_thesis: F1 . h = F2 . h then reconsider H = h as strict Subgroup of G by GROUP_3:def_1; thus F1 . h = the carrier of H by A3 .= F2 . h by A4 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines carr LATSUBGR:def_1_:_ for G being Group for b2 being Function of (Subgroups G),(bool the carrier of G) holds ( b2 = carr G iff for H being strict Subgroup of G holds b2 . H = the carrier of H ); 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 ) proof let G be Group; ::_thesis: for H being strict Subgroup of G for x being Element of G holds ( x in (carr G) . H iff x in H ) let H be strict Subgroup of G; ::_thesis: for x being Element of G holds ( x in (carr G) . H iff x in H ) let x be Element of G; ::_thesis: ( x in (carr G) . H iff x in H ) thus ( x in (carr G) . H implies x in H ) ::_thesis: ( x in H implies x in (carr G) . H ) proof assume x in (carr G) . H ; ::_thesis: x in H then x in the carrier of H by Def1; hence x in H by STRUCT_0:def_5; ::_thesis: verum end; assume A1: x in H ; ::_thesis: x in (carr G) . H (carr G) . H = the carrier of H by Def1; hence x in (carr G) . H by A1, STRUCT_0:def_5; ::_thesis: verum end; theorem :: LATSUBGR:14 for G being Group for H being strict Subgroup of G holds 1_ G in (carr G) . H proof let G be Group; ::_thesis: for H being strict Subgroup of G holds 1_ G in (carr G) . H let H be strict Subgroup of G; ::_thesis: 1_ G in (carr G) . H ( (carr G) . H = the carrier of H & 1_ H = 1_ G ) by Def1, GROUP_2:44; hence 1_ G in (carr G) . H ; ::_thesis: verum end; theorem :: LATSUBGR:15 for G being Group for H being strict Subgroup of G holds (carr G) . H <> {} by Def1; 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 proof let G be Group; ::_thesis: 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 let H be strict Subgroup of G; ::_thesis: 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 let g1, g2 be Element of G; ::_thesis: ( g1 in (carr G) . H & g2 in (carr G) . H implies g1 * g2 in (carr G) . H ) assume ( g1 in (carr G) . H & g2 in (carr G) . H ) ; ::_thesis: g1 * g2 in (carr G) . H then ( g1 in H & g2 in H ) by Th13; then g1 * g2 in H by GROUP_2:50; hence g1 * g2 in (carr G) . H by Th13; ::_thesis: verum 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 proof let G be Group; ::_thesis: 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 let H be strict Subgroup of G; ::_thesis: for g being Element of G st g in (carr G) . H holds g " in (carr G) . H let g be Element of G; ::_thesis: ( g in (carr G) . H implies g " in (carr G) . H ) assume g in (carr G) . H ; ::_thesis: g " in (carr G) . H then g in H by Th13; then g " in H by GROUP_2:51; hence g " in (carr G) . H by Th13; ::_thesis: verum 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) proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) let H1, H2 be strict Subgroup of G; ::_thesis: the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) ( (carr G) . H1 = the carrier of H1 & (carr G) . H2 = the carrier of H2 ) by Def1; hence the carrier of (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) by Th1; ::_thesis: verum 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) proof let G be Group; ::_thesis: for H1, H2 being strict Subgroup of G holds (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) let H1, H2 be strict Subgroup of G; ::_thesis: (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) ((carr G) . H1) /\ ((carr G) . H2) = the carrier of (H1 /\ H2) by Th18; hence (carr G) . (H1 /\ H2) = ((carr G) . H1) /\ ((carr G) . H2) by Def1; ::_thesis: verum end; definition let G be Group; 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 ex b1 being strict Subgroup of G st the carrier of b1 = meet ((carr G) .: F) proof reconsider CG = (carr G) .: F as Subset-Family of G ; A1: (carr G) .: F <> {} proof consider x being Element of Subgroups G such that A2: x in F by SUBSET_1:4; (carr G) . x in (carr G) .: F by A2, FUNCT_2:35; hence (carr G) .: F <> {} ; ::_thesis: verum end; A3: for g being Element of G st g in meet CG holds g " in meet CG proof let g be Element of G; ::_thesis: ( g in meet CG implies g " in meet CG ) assume A4: g in meet CG ; ::_thesis: g " in meet CG for X being set st X in (carr G) .: F holds g " in X proof reconsider h = g as Element of G ; let X be set ; ::_thesis: ( X in (carr G) .: F implies g " in X ) assume A5: X in (carr G) .: F ; ::_thesis: g " in X then A6: g in X by A4, SETFAM_1:def_1; reconsider X = X as Subset of G by A5; consider X1 being Element of Subgroups G such that X1 in F and A7: X = (carr G) . X1 by A5, FUNCT_2:65; reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def_1; A8: X = the carrier of X1 by A7, Def1; then h in X1 by A6, STRUCT_0:def_5; then h " in X1 by GROUP_2:51; hence g " in X by A8, STRUCT_0:def_5; ::_thesis: verum end; hence g " in meet CG by A1, SETFAM_1:def_1; ::_thesis: verum end; A9: for g1, g2 being Element of G st g1 in meet ((carr G) .: F) & g2 in meet ((carr G) .: F) holds g1 * g2 in meet ((carr G) .: F) proof let g1, g2 be Element of G; ::_thesis: ( g1 in meet ((carr G) .: F) & g2 in meet ((carr G) .: F) implies g1 * g2 in meet ((carr G) .: F) ) assume that A10: g1 in meet ((carr G) .: F) and A11: g2 in meet ((carr G) .: F) ; ::_thesis: g1 * g2 in meet ((carr G) .: F) for X being set st X in (carr G) .: F holds g1 * g2 in X proof reconsider h1 = g1, h2 = g2 as Element of G ; let X be set ; ::_thesis: ( X in (carr G) .: F implies g1 * g2 in X ) assume A12: X in (carr G) .: F ; ::_thesis: g1 * g2 in X then A13: g1 in X by A10, SETFAM_1:def_1; A14: g2 in X by A11, A12, SETFAM_1:def_1; reconsider X = X as Subset of G by A12; consider X1 being Element of Subgroups G such that X1 in F and A15: X = (carr G) . X1 by A12, FUNCT_2:65; reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def_1; A16: X = the carrier of X1 by A15, Def1; then A17: h2 in X1 by A14, STRUCT_0:def_5; h1 in X1 by A13, A16, STRUCT_0:def_5; then h1 * h2 in X1 by A17, GROUP_2:50; hence g1 * g2 in X by A16, STRUCT_0:def_5; ::_thesis: verum end; hence g1 * g2 in meet ((carr G) .: F) by A1, SETFAM_1:def_1; ::_thesis: verum end; for X being set st X in (carr G) .: F holds 1_ G in X proof let X be set ; ::_thesis: ( X in (carr G) .: F implies 1_ G in X ) assume A18: X in (carr G) .: F ; ::_thesis: 1_ G in X then reconsider X = X as Subset of G ; consider X1 being Element of Subgroups G such that X1 in F and A19: X = (carr G) . X1 by A18, FUNCT_2:65; reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def_1; A20: 1_ G in X1 by GROUP_2:46; X = the carrier of X1 by A19, Def1; hence 1_ G in X by A20, STRUCT_0:def_5; ::_thesis: verum end; then meet ((carr G) .: F) <> {} by A1, SETFAM_1:def_1; hence ex b1 being strict Subgroup of G st the carrier of b1 = meet ((carr G) .: F) by A9, A3, GROUP_2:52; ::_thesis: verum end; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = meet ((carr G) .: F) & the carrier of b2 = meet ((carr G) .: F) holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def2 defines meet LATSUBGR:def_2_:_ for G being Group for F being non empty Subset of (Subgroups G) for b3 being strict Subgroup of G holds ( b3 = meet F iff the carrier of b3 = meet ((carr G) .: F) ); 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 proof let G be Group; ::_thesis: for F being non empty Subset of (Subgroups G) st (1). G in F holds meet F = (1). G let F be non empty Subset of (Subgroups G); ::_thesis: ( (1). G in F implies meet F = (1). G ) assume A1: (1). G in F ; ::_thesis: meet F = (1). G reconsider 1G = (1). G as Element of Subgroups G by GROUP_3:def_1; (carr G) . 1G = the carrier of ((1). G) by Def1; then the carrier of ((1). G) in (carr G) .: F by A1, FUNCT_2:35; then {(1_ G)} in (carr G) .: F by GROUP_2:def_7; then meet ((carr G) .: F) c= {(1_ G)} by SETFAM_1:3; then A2: the carrier of (meet F) c= {(1_ G)} by Def2; (1). G is Subgroup of meet F by GROUP_2:65; then the carrier of ((1). G) c= the carrier of (meet F) by GROUP_2:def_5; then {(1_ G)} c= the carrier of (meet F) by GROUP_2:def_7; then the carrier of (meet F) = {(1_ G)} by A2, XBOOLE_0:def_10; hence meet F = (1). G by GROUP_2:def_7; ::_thesis: verum 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 proof let G be Group; ::_thesis: for h being Element of Subgroups G for F being non empty Subset of (Subgroups G) st F = {h} holds meet F = h let h be Element of Subgroups G; ::_thesis: for F being non empty Subset of (Subgroups G) st F = {h} holds meet F = h let F be non empty Subset of (Subgroups G); ::_thesis: ( F = {h} implies meet F = h ) assume A1: F = {h} ; ::_thesis: meet F = h reconsider H = h as strict Subgroup of G by GROUP_3:def_1; h in Subgroups G ; then h in dom (carr G) by FUNCT_2:def_1; then meet (Im ((carr G),h)) = meet {((carr G) . h)} by FUNCT_1:59; then A2: meet (Im ((carr G),h)) = (carr G) . h by SETFAM_1:10; the carrier of (meet F) = meet ((carr G) .: F) by Def2; then the carrier of (meet F) = the carrier of H by A1, A2, Def1; hence meet F = h by GROUP_2:59; ::_thesis: verum 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 proof let G be Group; ::_thesis: 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 let H1, H2 be Subgroup of G; ::_thesis: for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds h1 "\/" h2 = H1 "\/" H2 let h1, h2 be Element of (lattice G); ::_thesis: ( h1 = H1 & h2 = H2 implies h1 "\/" h2 = H1 "\/" H2 ) A1: h1 "\/" h2 = (SubJoin G) . (h1,h2) by LATTICES:def_1; assume A2: ( h1 = H1 & h2 = H2 ) ; ::_thesis: h1 "\/" h2 = H1 "\/" H2 then ( H1 is strict & H2 is strict ) by GROUP_3:def_1; hence h1 "\/" h2 = H1 "\/" H2 by A2, A1, GROUP_4:def_10; ::_thesis: verum 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 proof let G be Group; ::_thesis: 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 let H1, H2 be Subgroup of G; ::_thesis: for h1, h2 being Element of (lattice G) st h1 = H1 & h2 = H2 holds h1 "/\" h2 = H1 /\ H2 let h1, h2 be Element of (lattice G); ::_thesis: ( h1 = H1 & h2 = H2 implies h1 "/\" h2 = H1 /\ H2 ) A1: h1 "/\" h2 = (SubMeet G) . (h1,h2) by LATTICES:def_2; assume A2: ( h1 = H1 & h2 = H2 ) ; ::_thesis: h1 "/\" h2 = H1 /\ H2 then ( H1 is strict & H2 is strict ) by GROUP_3:def_1; hence h1 "/\" h2 = H1 /\ H2 by A2, A1, GROUP_4:def_11; ::_thesis: verum end; theorem :: LATSUBGR:24 for G being Group for p being Element of (lattice G) for H being Subgroup of G st p = H holds H is strict Subgroup of G by GROUP_3:def_1; 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 ) proof let G be Group; ::_thesis: 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 ) let H1, H2 be Subgroup of G; ::_thesis: 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 ) let p, q be Element of (lattice G); ::_thesis: ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) ) assume that A1: p = H1 and A2: q = H2 ; ::_thesis: ( p [= q iff the carrier of H1 c= the carrier of H2 ) A3: H1 is strict Subgroup of G by A1, GROUP_3:def_1; A4: H2 is strict Subgroup of G by A2, GROUP_3:def_1; thus ( p [= q implies the carrier of H1 c= the carrier of H2 ) ::_thesis: ( the carrier of H1 c= the carrier of H2 implies p [= q ) proof assume p [= q ; ::_thesis: the carrier of H1 c= the carrier of H2 then A5: p "/\" q = p by LATTICES:4; p "/\" q = the L_meet of (lattice G) . (p,q) by LATTICES:def_2 .= H1 /\ H2 by A1, A2, A3, A4, GROUP_4:def_11 ; then the carrier of H1 /\ the carrier of H2 = the carrier of H1 by A1, A5, Th1; hence the carrier of H1 c= the carrier of H2 by XBOOLE_1:17; ::_thesis: verum end; thus ( the carrier of H1 c= the carrier of H2 implies p [= q ) ::_thesis: verum proof assume the carrier of H1 c= the carrier of H2 ; ::_thesis: p [= q then H1 is Subgroup of H2 by GROUP_2:57; then A6: H1 /\ H2 = H1 by A3, GROUP_2:89; H1 /\ H2 = the L_meet of (lattice G) . (p,q) by A1, A2, A3, A4, GROUP_4:def_11 .= p "/\" q by LATTICES:def_2 ; hence p [= q by A1, A6, LATTICES:4; ::_thesis: verum end; 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 ) proof let G be Group; ::_thesis: 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 ) let H1, H2 be Subgroup of G; ::_thesis: for p, q being Element of (lattice G) st p = H1 & q = H2 holds ( p [= q iff H1 is Subgroup of H2 ) let p, q be Element of (lattice G); ::_thesis: ( p = H1 & q = H2 implies ( p [= q iff H1 is Subgroup of H2 ) ) assume that A1: p = H1 and A2: q = H2 ; ::_thesis: ( p [= q iff H1 is Subgroup of H2 ) thus ( p [= q implies H1 is Subgroup of H2 ) ::_thesis: ( H1 is Subgroup of H2 implies p [= q ) proof assume p [= q ; ::_thesis: H1 is Subgroup of H2 then the carrier of H1 c= the carrier of H2 by A1, A2, Th25; hence H1 is Subgroup of H2 by GROUP_2:57; ::_thesis: verum end; A3: H1 is strict Subgroup of G by A1, GROUP_3:def_1; A4: H2 is strict Subgroup of G by A2, GROUP_3:def_1; thus ( H1 is Subgroup of H2 implies p [= q ) ::_thesis: verum proof assume H1 is Subgroup of H2 ; ::_thesis: p [= q then A5: H1 /\ H2 = H1 by A3, GROUP_2:89; H1 /\ H2 = the L_meet of (lattice G) . (p,q) by A1, A2, A3, A4, GROUP_4:def_11 .= p "/\" q by LATTICES:def_2 ; hence p [= q by A1, A5, LATTICES:4; ::_thesis: verum end; end; theorem :: LATSUBGR:27 for G being Group holds lattice G is complete proof let G be Group; ::_thesis: lattice G is complete let Y be Subset of (lattice G); :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of (lattice G) st ( b1 is_less_than Y & ( for b2 being Element of the carrier of (lattice G) holds ( not b2 is_less_than Y or b2 [= b1 ) ) ) percases ( Y = {} or Y <> {} ) ; supposeA1: Y = {} ; ::_thesis: ex b1 being Element of the carrier of (lattice G) st ( b1 is_less_than Y & ( for b2 being Element of the carrier of (lattice G) holds ( not b2 is_less_than Y or b2 [= b1 ) ) ) take Top (lattice G) ; ::_thesis: ( Top (lattice G) is_less_than Y & ( for b1 being Element of the carrier of (lattice G) holds ( not b1 is_less_than Y or b1 [= Top (lattice G) ) ) ) thus Top (lattice G) is_less_than Y ::_thesis: for b1 being Element of the carrier of (lattice G) holds ( not b1 is_less_than Y or b1 [= Top (lattice G) ) proof let q be Element of (lattice G); :: according to LATTICE3:def_16 ::_thesis: ( not q in Y or Top (lattice G) [= q ) thus ( not q in Y or Top (lattice G) [= q ) by A1; ::_thesis: verum end; let b be Element of (lattice G); ::_thesis: ( not b is_less_than Y or b [= Top (lattice G) ) assume b is_less_than Y ; ::_thesis: b [= Top (lattice G) thus b [= Top (lattice G) by LATTICES:19; ::_thesis: verum end; suppose Y <> {} ; ::_thesis: ex b1 being Element of the carrier of (lattice G) st ( b1 is_less_than Y & ( for b2 being Element of the carrier of (lattice G) holds ( not b2 is_less_than Y or b2 [= b1 ) ) ) then reconsider X = Y as non empty Subset of (Subgroups G) ; reconsider p = meet X as Element of (lattice G) by GROUP_3:def_1; take p ; ::_thesis: ( p is_less_than Y & ( for b1 being Element of the carrier of (lattice G) holds ( not b1 is_less_than Y or b1 [= p ) ) ) set x = the Element of X; thus p is_less_than Y ::_thesis: for b1 being Element of the carrier of (lattice G) holds ( not b1 is_less_than Y or b1 [= p ) proof let q be Element of (lattice G); :: according to LATTICE3:def_16 ::_thesis: ( not q in Y or p [= q ) reconsider H = q as strict Subgroup of G by GROUP_3:def_1; reconsider h = q as Element of Subgroups G ; assume A2: q in Y ; ::_thesis: p [= q (carr G) . h = the carrier of H by Def1; then meet ((carr G) .: X) c= the carrier of H by A2, FUNCT_2:35, SETFAM_1:3; then the carrier of (meet X) c= the carrier of H by Def2; hence p [= q by Th25; ::_thesis: verum end; let r be Element of (lattice G); ::_thesis: ( not r is_less_than Y or r [= p ) reconsider H = r as Subgroup of G by GROUP_3:def_1; assume A3: r is_less_than Y ; ::_thesis: r [= p A4: for Z1 being set st Z1 in (carr G) .: X holds the carrier of H c= Z1 proof let Z1 be set ; ::_thesis: ( Z1 in (carr G) .: X implies the carrier of H c= Z1 ) assume A5: Z1 in (carr G) .: X ; ::_thesis: the carrier of H c= Z1 then reconsider Z2 = Z1 as Subset of G ; consider z1 being Element of Subgroups G such that A6: ( z1 in X & Z2 = (carr G) . z1 ) by A5, FUNCT_2:65; reconsider z1 = z1 as Element of (lattice G) ; reconsider z3 = z1 as strict Subgroup of G by GROUP_3:def_1; ( Z1 = the carrier of z3 & r [= z1 ) by A3, A6, Def1, LATTICE3:def_16; hence the carrier of H c= Z1 by Th25; ::_thesis: verum end; (carr G) . the Element of X in (carr G) .: X by FUNCT_2:35; then the carrier of H c= meet ((carr G) .: X) by A4, SETFAM_1:5; then the carrier of H c= the carrier of (meet X) by Def2; hence r [= p by Th25; ::_thesis: verum end; end; end; definition let G1, G2 be Group; 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 ex b1 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 b1 . H = gr A proof defpred S1[ set , set ] means for H being strict Subgroup of G1 st H = \$1 holds for A being Subset of G2 st A = f .: the carrier of H holds \$2 = gr (f .: the carrier of H); A1: for e being set st e in the carrier of (lattice G1) holds ex u being set st ( u in the carrier of (lattice G2) & S1[e,u] ) proof let e be set ; ::_thesis: ( e in the carrier of (lattice G1) implies ex u being set st ( u in the carrier of (lattice G2) & S1[e,u] ) ) assume e in the carrier of (lattice G1) ; ::_thesis: ex u being set st ( u in the carrier of (lattice G2) & S1[e,u] ) then reconsider E = e as strict Subgroup of G1 by GROUP_3:def_1; reconsider u = gr (f .: the carrier of E) as strict Subgroup of G2 ; reconsider u = u as Element of (lattice G2) by GROUP_3:def_1; take u ; ::_thesis: ( u in the carrier of (lattice G2) & S1[e,u] ) thus ( u in the carrier of (lattice G2) & S1[e,u] ) ; ::_thesis: verum end; consider f1 being Function of the carrier of (lattice G1), the carrier of (lattice G2) such that A2: for e being set st e in the carrier of (lattice G1) holds S1[e,f1 . e] from FUNCT_2:sch_1(A1); take f1 ; ::_thesis: for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds f1 . H = gr A let H be strict Subgroup of G1; ::_thesis: for A being Subset of G2 st A = f .: the carrier of H holds f1 . H = gr A let A be Subset of G2; ::_thesis: ( A = f .: the carrier of H implies f1 . H = gr A ) A3: H in the carrier of (lattice G1) by GROUP_3:def_1; assume A = f .: the carrier of H ; ::_thesis: f1 . H = gr A hence f1 . H = gr A by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 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 b1 . H = gr A ) & ( for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds b2 . H = gr A ) holds b1 = b2 proof let f1, f2 be Function of the carrier of (lattice G1), the carrier of (lattice G2); ::_thesis: ( ( for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds f1 . H = gr A ) & ( for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds f2 . H = gr A ) implies f1 = f2 ) assume that A4: for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds f1 . H = gr A and A5: for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds f2 . H = gr A ; ::_thesis: f1 = f2 for h being set st h in the carrier of (lattice G1) holds f1 . h = f2 . h proof let h be set ; ::_thesis: ( h in the carrier of (lattice G1) implies f1 . h = f2 . h ) assume h in the carrier of (lattice G1) ; ::_thesis: f1 . h = f2 . h then reconsider H = h as strict Subgroup of G1 by GROUP_3:def_1; thus f1 . h = gr (f .: the carrier of H) by A4 .= f2 . h by A5 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; 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 b4 being Function of the carrier of (lattice G1), the carrier of (lattice G2) holds ( b4 = FuncLatt f iff for H being strict Subgroup of G1 for A being Subset of G2 st A = f .: the carrier of H holds b4 . H = gr A ); theorem :: LATSUBGR:28 for G being Group holds FuncLatt (id the carrier of G) = id the carrier of (lattice G) proof let G be Group; ::_thesis: FuncLatt (id the carrier of G) = id the carrier of (lattice G) set f = id the carrier of G; A1: for x being set st x in the carrier of (lattice G) holds (FuncLatt (id the carrier of G)) . x = x proof let x be set ; ::_thesis: ( x in the carrier of (lattice G) implies (FuncLatt (id the carrier of G)) . x = x ) assume x in the carrier of (lattice G) ; ::_thesis: (FuncLatt (id the carrier of G)) . x = x then reconsider x = x as strict Subgroup of G by GROUP_3:def_1; A2: the carrier of x c= (id the carrier of G) .: the carrier of x proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of x or z in (id the carrier of G) .: the carrier of x ) assume A3: z in the carrier of x ; ::_thesis: z in (id the carrier of G) .: the carrier of x the carrier of x c= the carrier of G by GROUP_2:def_5; then reconsider z = z as Element of G by A3; (id the carrier of G) . z = z by FUNCT_1:17; hence z in (id the carrier of G) .: the carrier of x by A3, FUNCT_2:35; ::_thesis: verum end; A4: (id the carrier of G) .: the carrier of x c= the carrier of x proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (id the carrier of G) .: the carrier of x or z in the carrier of x ) assume A5: z in (id the carrier of G) .: the carrier of x ; ::_thesis: z in the carrier of x then reconsider z = z as Element of G ; ex Z being Element of G st ( Z in the carrier of x & z = (id the carrier of G) . Z ) by A5, FUNCT_2:65; hence z in the carrier of x by FUNCT_1:17; ::_thesis: verum end; then reconsider X = the carrier of x as Subset of G by A2, XBOOLE_0:def_10; (id the carrier of G) .: the carrier of x = the carrier of x by A4, A2, XBOOLE_0:def_10; then (FuncLatt (id the carrier of G)) . x = gr X by Def3; hence (FuncLatt (id the carrier of G)) . x = x by Th3; ::_thesis: verum end; dom (FuncLatt (id the carrier of G)) = the carrier of (lattice G) by FUNCT_2:def_1; hence FuncLatt (id the carrier of G) = id the carrier of (lattice G) by A1, FUNCT_1:17; ::_thesis: verum end; 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 proof let G1, G2 be Group; ::_thesis: for f being Homomorphism of G1,G2 st f is one-to-one holds FuncLatt f is one-to-one let f be Homomorphism of G1,G2; ::_thesis: ( f is one-to-one implies FuncLatt f is one-to-one ) assume A1: f is one-to-one ; ::_thesis: FuncLatt f is one-to-one for x1, x2 being set st x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 holds x1 = x2 proof reconsider y = f . (1_ G1) as Element of G2 ; let x1, x2 be set ; ::_thesis: ( x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 implies x1 = x2 ) assume that A2: ( x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) ) and A3: (FuncLatt f) . x1 = (FuncLatt f) . x2 ; ::_thesis: x1 = x2 reconsider x1 = x1, x2 = x2 as strict Subgroup of G1 by A2, GROUP_3:def_1; reconsider A1 = f .: the carrier of x1, A2 = f .: the carrier of x2 as Subset of G2 ; A4: for g being Element of G2 st g in f .: the carrier of x1 holds g " in f .: the carrier of x1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of x1 implies g " in f .: the carrier of x1 ) assume g in f .: the carrier of x1 ; ::_thesis: g " in f .: the carrier of x1 then consider x being Element of G1 such that A5: x in the carrier of x1 and A6: g = f . x by FUNCT_2:65; x in x1 by A5, STRUCT_0:def_5; then x " in x1 by GROUP_2:51; then A7: x " in the carrier of x1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of x1 by A6, A7, FUNCT_2:35; ::_thesis: verum end; A8: for g1, g2 being Element of G2 st g1 in f .: the carrier of x1 & g2 in f .: the carrier of x1 holds g1 * g2 in f .: the carrier of x1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of x1 & g2 in f .: the carrier of x1 implies g1 * g2 in f .: the carrier of x1 ) assume that A9: g1 in f .: the carrier of x1 and A10: g2 in f .: the carrier of x1 ; ::_thesis: g1 * g2 in f .: the carrier of x1 consider x being Element of G1 such that A11: x in the carrier of x1 and A12: g1 = f . x by A9, FUNCT_2:65; consider y being Element of G1 such that A13: y in the carrier of x1 and A14: g2 = f . y by A10, FUNCT_2:65; A15: y in x1 by A13, STRUCT_0:def_5; x in x1 by A11, STRUCT_0:def_5; then x * y in x1 by A15, GROUP_2:50; then A16: x * y in the carrier of x1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of x1 by A12, A14, A16, FUNCT_2:35; ::_thesis: verum end; A17: for g being Element of G2 st g in f .: the carrier of x2 holds g " in f .: the carrier of x2 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of x2 implies g " in f .: the carrier of x2 ) assume g in f .: the carrier of x2 ; ::_thesis: g " in f .: the carrier of x2 then consider x being Element of G1 such that A18: x in the carrier of x2 and A19: g = f . x by FUNCT_2:65; x in x2 by A18, STRUCT_0:def_5; then x " in x2 by GROUP_2:51; then A20: x " in the carrier of x2 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of x2 by A19, A20, FUNCT_2:35; ::_thesis: verum end; A21: dom f = the carrier of G1 by FUNCT_2:def_1; A22: for g1, g2 being Element of G2 st g1 in f .: the carrier of x2 & g2 in f .: the carrier of x2 holds g1 * g2 in f .: the carrier of x2 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of x2 & g2 in f .: the carrier of x2 implies g1 * g2 in f .: the carrier of x2 ) assume that A23: g1 in f .: the carrier of x2 and A24: g2 in f .: the carrier of x2 ; ::_thesis: g1 * g2 in f .: the carrier of x2 consider x being Element of G1 such that A25: x in the carrier of x2 and A26: g1 = f . x by A23, FUNCT_2:65; consider y being Element of G1 such that A27: y in the carrier of x2 and A28: g2 = f . y by A24, FUNCT_2:65; A29: y in x2 by A27, STRUCT_0:def_5; x in x2 by A25, STRUCT_0:def_5; then x * y in x2 by A29, GROUP_2:50; then A30: x * y in the carrier of x2 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of x2 by A26, A28, A30, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in x2 by GROUP_2:46; then A31: 1_ G1 in the carrier of x2 by STRUCT_0:def_5; A32: ( (FuncLatt f) . x1 = gr A1 & (FuncLatt f) . x2 = gr A2 ) by Def3; ex y being Element of G2 st y = f . (1_ G1) ; then f .: the carrier of x2 <> {} by A21, A31, FUNCT_1:def_6; then consider B2 being strict Subgroup of G2 such that A33: the carrier of B2 = f .: the carrier of x2 by A17, A22, GROUP_2:52; 1_ G1 in x1 by GROUP_2:46; then 1_ G1 in the carrier of x1 by STRUCT_0:def_5; then y in f .: the carrier of x1 by A21, FUNCT_1:def_6; then A34: ex B1 being strict Subgroup of G2 st the carrier of B1 = f .: the carrier of x1 by A4, A8, GROUP_2:52; gr (f .: the carrier of x2) = B2 by A33, Th3; then A35: f .: the carrier of x1 = f .: the carrier of x2 by A3, A32, A34, A33, Th3; the carrier of x2 c= dom f by A21, GROUP_2:def_5; then A36: the carrier of x2 c= the carrier of x1 by A1, A35, FUNCT_1:87; the carrier of x1 c= dom f by A21, GROUP_2:def_5; then the carrier of x1 c= the carrier of x2 by A1, A35, FUNCT_1:87; then the carrier of x1 = the carrier of x2 by A36, XBOOLE_0:def_10; hence x1 = x2 by GROUP_2:59; ::_thesis: verum end; hence FuncLatt f is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; theorem :: LATSUBGR:30 for G1, G2 being Group for f being Homomorphism of G1,G2 holds (FuncLatt f) . ((1). G1) = (1). G2 proof let G1, G2 be Group; ::_thesis: for f being Homomorphism of G1,G2 holds (FuncLatt f) . ((1). G1) = (1). G2 let f be Homomorphism of G1,G2; ::_thesis: (FuncLatt f) . ((1). G1) = (1). G2 consider A being Subset of G2 such that A1: A = f .: the carrier of ((1). G1) ; A2: A = f .: {(1_ G1)} by A1, GROUP_2:def_7; A3: ( 1_ G1 in {(1_ G1)} & 1_ G2 = f . (1_ G1) ) by GROUP_6:31, TARSKI:def_1; for x being set holds ( x in A iff x = 1_ G2 ) proof let x be set ; ::_thesis: ( x in A iff x = 1_ G2 ) thus ( x in A implies x = 1_ G2 ) ::_thesis: ( x = 1_ G2 implies x in A ) proof assume A4: x in A ; ::_thesis: x = 1_ G2 then reconsider x = x as Element of G2 ; consider y being Element of G1 such that A5: y in {(1_ G1)} and A6: x = f . y by A2, A4, FUNCT_2:65; y = 1_ G1 by A5, TARSKI:def_1; hence x = 1_ G2 by A6, GROUP_6:31; ::_thesis: verum end; thus ( x = 1_ G2 implies x in A ) by A2, A3, FUNCT_2:35; ::_thesis: verum end; then A = {(1_ G2)} by TARSKI:def_1; then gr A = (1). G2 by Th12; hence (FuncLatt f) . ((1). G1) = (1). G2 by A1, Def3; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: for f being Homomorphism of G1,G2 st f is one-to-one holds FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 let f be Homomorphism of G1,G2; ::_thesis: ( f is one-to-one implies FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 ) assume A1: f is one-to-one ; ::_thesis: FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 for a, b being Element of (lattice G1) holds (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) proof let a, b be Element of (lattice G1); ::_thesis: (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) consider A1 being strict Subgroup of G1 such that A2: A1 = a by Th2; consider B1 being strict Subgroup of G1 such that A3: B1 = b by Th2; thus (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) ::_thesis: verum proof A4: for g1, g2 being Element of G2 st g1 in f .: the carrier of B1 & g2 in f .: the carrier of B1 holds g1 * g2 in f .: the carrier of B1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of B1 & g2 in f .: the carrier of B1 implies g1 * g2 in f .: the carrier of B1 ) assume that A5: g1 in f .: the carrier of B1 and A6: g2 in f .: the carrier of B1 ; ::_thesis: g1 * g2 in f .: the carrier of B1 consider x being Element of G1 such that A7: x in the carrier of B1 and A8: g1 = f . x by A5, FUNCT_2:65; consider y being Element of G1 such that A9: y in the carrier of B1 and A10: g2 = f . y by A6, FUNCT_2:65; A11: y in B1 by A9, STRUCT_0:def_5; x in B1 by A7, STRUCT_0:def_5; then x * y in B1 by A11, GROUP_2:50; then A12: x * y in the carrier of B1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of B1 by A8, A10, A12, FUNCT_2:35; ::_thesis: verum end; A13: for g being Element of G2 st g in f .: the carrier of B1 holds g " in f .: the carrier of B1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of B1 implies g " in f .: the carrier of B1 ) assume g in f .: the carrier of B1 ; ::_thesis: g " in f .: the carrier of B1 then consider x being Element of G1 such that A14: x in the carrier of B1 and A15: g = f . x by FUNCT_2:65; x in B1 by A14, STRUCT_0:def_5; then x " in B1 by GROUP_2:51; then A16: x " in the carrier of B1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of B1 by A15, A16, FUNCT_2:35; ::_thesis: verum end; A17: for g being Element of G2 st g in f .: the carrier of A1 holds g " in f .: the carrier of A1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of A1 implies g " in f .: the carrier of A1 ) assume g in f .: the carrier of A1 ; ::_thesis: g " in f .: the carrier of A1 then consider x being Element of G1 such that A18: x in the carrier of A1 and A19: g = f . x by FUNCT_2:65; x in A1 by A18, STRUCT_0:def_5; then x " in A1 by GROUP_2:51; then A20: x " in the carrier of A1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of A1 by A19, A20, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in A1 by GROUP_2:46; then A21: 1_ G1 in the carrier of A1 by STRUCT_0:def_5; A22: (FuncLatt f) . (A1 /\ B1) = gr (f .: the carrier of (A1 /\ B1)) by Def3; consider C1 being strict Subgroup of G1 such that A23: C1 = A1 /\ B1 ; A24: for g1, g2 being Element of G2 st g1 in f .: the carrier of A1 & g2 in f .: the carrier of A1 holds g1 * g2 in f .: the carrier of A1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of A1 & g2 in f .: the carrier of A1 implies g1 * g2 in f .: the carrier of A1 ) assume that A25: g1 in f .: the carrier of A1 and A26: g2 in f .: the carrier of A1 ; ::_thesis: g1 * g2 in f .: the carrier of A1 consider x being Element of G1 such that A27: x in the carrier of A1 and A28: g1 = f . x by A25, FUNCT_2:65; consider y being Element of G1 such that A29: y in the carrier of A1 and A30: g2 = f . y by A26, FUNCT_2:65; A31: y in A1 by A29, STRUCT_0:def_5; x in A1 by A27, STRUCT_0:def_5; then x * y in A1 by A31, GROUP_2:50; then A32: x * y in the carrier of A1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of A1 by A28, A30, A32, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in B1 by GROUP_2:46; then A33: 1_ G1 in the carrier of B1 by STRUCT_0:def_5; A34: ( (FuncLatt f) . a = gr (f .: the carrier of A1) & (FuncLatt f) . b = gr (f .: the carrier of B1) ) by A2, A3, Def3; A35: dom f = the carrier of G1 by FUNCT_2:def_1; A36: for g1, g2 being Element of G2 st g1 in f .: the carrier of C1 & g2 in f .: the carrier of C1 holds g1 * g2 in f .: the carrier of C1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of C1 & g2 in f .: the carrier of C1 implies g1 * g2 in f .: the carrier of C1 ) assume that A37: g1 in f .: the carrier of C1 and A38: g2 in f .: the carrier of C1 ; ::_thesis: g1 * g2 in f .: the carrier of C1 consider x being Element of G1 such that A39: x in the carrier of C1 and A40: g1 = f . x by A37, FUNCT_2:65; consider y being Element of G1 such that A41: y in the carrier of C1 and A42: g2 = f . y by A38, FUNCT_2:65; A43: y in C1 by A41, STRUCT_0:def_5; x in C1 by A39, STRUCT_0:def_5; then x * y in C1 by A43, GROUP_2:50; then A44: x * y in the carrier of C1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of C1 by A40, A42, A44, FUNCT_2:35; ::_thesis: verum end; A45: for g being Element of G2 st g in f .: the carrier of C1 holds g " in f .: the carrier of C1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of C1 implies g " in f .: the carrier of C1 ) assume g in f .: the carrier of C1 ; ::_thesis: g " in f .: the carrier of C1 then consider x being Element of G1 such that A46: x in the carrier of C1 and A47: g = f . x by FUNCT_2:65; x in C1 by A46, STRUCT_0:def_5; then x " in C1 by GROUP_2:51; then A48: x " in the carrier of C1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of C1 by A47, A48, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in C1 by GROUP_2:46; then A49: 1_ G1 in the carrier of C1 by STRUCT_0:def_5; ex y2 being Element of G2 st y2 = f . (1_ G1) ; then f .: the carrier of C1 <> {} by A35, A49, FUNCT_1:def_6; then consider C3 being strict Subgroup of G2 such that A50: the carrier of C3 = f .: the carrier of C1 by A45, A36, GROUP_2:52; ex y1 being Element of G2 st y1 = f . (1_ G1) ; then f .: the carrier of B1 <> {} by A35, A33, FUNCT_1:def_6; then consider B3 being strict Subgroup of G2 such that A51: the carrier of B3 = f .: the carrier of B1 by A13, A4, GROUP_2:52; ex y being Element of G2 st y = f . (1_ G1) ; then f .: the carrier of A1 <> {} by A35, A21, FUNCT_1:def_6; then consider A3 being strict Subgroup of G2 such that A52: the carrier of A3 = f .: the carrier of A1 by A17, A24, GROUP_2:52; A53: the carrier of C3 c= the carrier of (A3 /\ B3) proof A54: f .: the carrier of (A1 /\ B1) c= f .: the carrier of B1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of (A1 /\ B1) or x in f .: the carrier of B1 ) assume A55: x in f .: the carrier of (A1 /\ B1) ; ::_thesis: x in f .: the carrier of B1 then reconsider x = x as Element of G2 ; consider y being Element of G1 such that A56: y in the carrier of (A1 /\ B1) and A57: x = f . y by A55, FUNCT_2:65; y in the carrier of A1 /\ the carrier of B1 by A56, Th1; then y in the carrier of B1 by XBOOLE_0:def_4; hence x in f .: the carrier of B1 by A57, FUNCT_2:35; ::_thesis: verum end; A58: f .: the carrier of (A1 /\ B1) c= f .: the carrier of A1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of (A1 /\ B1) or x in f .: the carrier of A1 ) assume A59: x in f .: the carrier of (A1 /\ B1) ; ::_thesis: x in f .: the carrier of A1 then reconsider x = x as Element of G2 ; consider y being Element of G1 such that A60: y in the carrier of (A1 /\ B1) and A61: x = f . y by A59, FUNCT_2:65; y in the carrier of A1 /\ the carrier of B1 by A60, Th1; then y in the carrier of A1 by XBOOLE_0:def_4; hence x in f .: the carrier of A1 by A61, FUNCT_2:35; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of C3 or x in the carrier of (A3 /\ B3) ) assume A62: x in the carrier of C3 ; ::_thesis: x in the carrier of (A3 /\ B3) the carrier of C3 c= the carrier of G2 by GROUP_2:def_5; then reconsider x = x as Element of G2 by A62; consider y being Element of G1 such that A63: y in the carrier of (A1 /\ B1) and A64: x = f . y by A23, A50, A62, FUNCT_2:65; f . y in f .: the carrier of (A1 /\ B1) by A63, FUNCT_2:35; then f . y in the carrier of A3 /\ the carrier of B3 by A52, A51, A58, A54, XBOOLE_0:def_4; hence x in the carrier of (A3 /\ B3) by A64, Th1; ::_thesis: verum end; A65: gr (f .: the carrier of B1) = B3 by A51, Th3; the carrier of (A3 /\ B3) c= the carrier of C3 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (A3 /\ B3) or x in the carrier of C3 ) assume x in the carrier of (A3 /\ B3) ; ::_thesis: x in the carrier of C3 then x in the carrier of A3 /\ the carrier of B3 by Th1; then x in f .: ( the carrier of A1 /\ the carrier of B1) by A1, A52, A51, FUNCT_1:62; hence x in the carrier of C3 by A23, A50, Th1; ::_thesis: verum end; then the carrier of (A3 /\ B3) = the carrier of C3 by A53, XBOOLE_0:def_10; then gr (f .: the carrier of (A1 /\ B1)) = A3 /\ B3 by A23, A50, Th3 .= (gr (f .: the carrier of A1)) /\ (gr (f .: the carrier of B1)) by A52, A65, Th3 .= ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) by A34, Th23 ; hence (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) by A2, A3, A22, Th23; ::_thesis: verum end; end; hence FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 by VECTSP_8:def_8; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: for f being Homomorphism of G1,G2 holds FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 let f be Homomorphism of G1,G2; ::_thesis: FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 for a, b being Element of (lattice G1) holds (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) proof let a, b be Element of (lattice G1); ::_thesis: (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) consider A1 being strict Subgroup of G1 such that A1: A1 = a by Th2; consider B1 being strict Subgroup of G1 such that A2: B1 = b by Th2; thus (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) ::_thesis: verum proof A3: for g being Element of G2 st g in f .: the carrier of B1 holds g " in f .: the carrier of B1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of B1 implies g " in f .: the carrier of B1 ) assume g in f .: the carrier of B1 ; ::_thesis: g " in f .: the carrier of B1 then consider x being Element of G1 such that A4: x in the carrier of B1 and A5: g = f . x by FUNCT_2:65; x in B1 by A4, STRUCT_0:def_5; then x " in B1 by GROUP_2:51; then A6: x " in the carrier of B1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of B1 by A5, A6, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in A1 by GROUP_2:46; then A7: 1_ G1 in the carrier of A1 by STRUCT_0:def_5; A8: ex y being Element of G2 st y = f . (1_ G1) ; ( the carrier of A1 c= the carrier of G1 & the carrier of B1 c= the carrier of G1 ) by GROUP_2:def_5; then reconsider A = the carrier of A1 \/ the carrier of B1 as Subset of G1 by XBOOLE_1:8; A9: for g being Element of G2 st g in f .: the carrier of A1 holds g " in f .: the carrier of A1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of A1 implies g " in f .: the carrier of A1 ) assume g in f .: the carrier of A1 ; ::_thesis: g " in f .: the carrier of A1 then consider x being Element of G1 such that A10: x in the carrier of A1 and A11: g = f . x by FUNCT_2:65; x in A1 by A10, STRUCT_0:def_5; then x " in A1 by GROUP_2:51; then A12: x " in the carrier of A1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of A1 by A11, A12, FUNCT_2:35; ::_thesis: verum end; reconsider B = (f .: the carrier of A1) \/ (f .: the carrier of B1) as Subset of G2 ; A13: dom f = the carrier of G1 by FUNCT_2:def_1; A14: for g1, g2 being Element of G2 st g1 in f .: the carrier of B1 & g2 in f .: the carrier of B1 holds g1 * g2 in f .: the carrier of B1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of B1 & g2 in f .: the carrier of B1 implies g1 * g2 in f .: the carrier of B1 ) assume that A15: g1 in f .: the carrier of B1 and A16: g2 in f .: the carrier of B1 ; ::_thesis: g1 * g2 in f .: the carrier of B1 consider x being Element of G1 such that A17: x in the carrier of B1 and A18: g1 = f . x by A15, FUNCT_2:65; consider y being Element of G1 such that A19: y in the carrier of B1 and A20: g2 = f . y by A16, FUNCT_2:65; A21: y in B1 by A19, STRUCT_0:def_5; x in B1 by A17, STRUCT_0:def_5; then x * y in B1 by A21, GROUP_2:50; then A22: x * y in the carrier of B1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of B1 by A18, A20, A22, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in B1 by GROUP_2:46; then A23: 1_ G1 in the carrier of B1 by STRUCT_0:def_5; A24: (FuncLatt f) . (A1 "\/" B1) = gr (f .: the carrier of (A1 "\/" B1)) by Def3; ex y1 being Element of G2 st y1 = f . (1_ G1) ; then f .: the carrier of B1 <> {} by A13, A23, FUNCT_1:def_6; then consider B3 being strict Subgroup of G2 such that A25: the carrier of B3 = f .: the carrier of B1 by A3, A14, GROUP_2:52; A26: for g1, g2 being Element of G2 st g1 in f .: the carrier of A1 & g2 in f .: the carrier of A1 holds g1 * g2 in f .: the carrier of A1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of A1 & g2 in f .: the carrier of A1 implies g1 * g2 in f .: the carrier of A1 ) assume that A27: g1 in f .: the carrier of A1 and A28: g2 in f .: the carrier of A1 ; ::_thesis: g1 * g2 in f .: the carrier of A1 consider x being Element of G1 such that A29: x in the carrier of A1 and A30: g1 = f . x by A27, FUNCT_2:65; consider y being Element of G1 such that A31: y in the carrier of A1 and A32: g2 = f . y by A28, FUNCT_2:65; A33: y in A1 by A31, STRUCT_0:def_5; x in A1 by A29, STRUCT_0:def_5; then x * y in A1 by A33, GROUP_2:50; then A34: x * y in the carrier of A1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of A1 by A30, A32, A34, FUNCT_2:35; ::_thesis: verum end; A35: ( (FuncLatt f) . a = gr (f .: the carrier of A1) & (FuncLatt f) . b = gr (f .: the carrier of B1) ) by A1, A2, Def3; consider C1 being strict Subgroup of G1 such that A36: C1 = A1 "\/" B1 ; A37: for g1, g2 being Element of G2 st g1 in f .: the carrier of C1 & g2 in f .: the carrier of C1 holds g1 * g2 in f .: the carrier of C1 proof let g1, g2 be Element of G2; ::_thesis: ( g1 in f .: the carrier of C1 & g2 in f .: the carrier of C1 implies g1 * g2 in f .: the carrier of C1 ) assume that A38: g1 in f .: the carrier of C1 and A39: g2 in f .: the carrier of C1 ; ::_thesis: g1 * g2 in f .: the carrier of C1 consider x being Element of G1 such that A40: x in the carrier of C1 and A41: g1 = f . x by A38, FUNCT_2:65; consider y being Element of G1 such that A42: y in the carrier of C1 and A43: g2 = f . y by A39, FUNCT_2:65; A44: y in C1 by A42, STRUCT_0:def_5; x in C1 by A40, STRUCT_0:def_5; then x * y in C1 by A44, GROUP_2:50; then A45: x * y in the carrier of C1 by STRUCT_0:def_5; f . (x * y) = (f . x) * (f . y) by GROUP_6:def_6; hence g1 * g2 in f .: the carrier of C1 by A41, A43, A45, FUNCT_2:35; ::_thesis: verum end; A46: for g being Element of G2 st g in f .: the carrier of C1 holds g " in f .: the carrier of C1 proof let g be Element of G2; ::_thesis: ( g in f .: the carrier of C1 implies g " in f .: the carrier of C1 ) assume g in f .: the carrier of C1 ; ::_thesis: g " in f .: the carrier of C1 then consider x being Element of G1 such that A47: x in the carrier of C1 and A48: g = f . x by FUNCT_2:65; x in C1 by A47, STRUCT_0:def_5; then x " in C1 by GROUP_2:51; then A49: x " in the carrier of C1 by STRUCT_0:def_5; f . (x ") = (f . x) " by GROUP_6:32; hence g " in f .: the carrier of C1 by A48, A49, FUNCT_2:35; ::_thesis: verum end; 1_ G1 in C1 by GROUP_2:46; then 1_ G1 in the carrier of C1 by STRUCT_0:def_5; then f .: the carrier of C1 <> {} by A13, A8, FUNCT_1:def_6; then consider C3 being strict Subgroup of G2 such that A50: the carrier of C3 = f .: the carrier of C1 by A46, A37, GROUP_2:52; ex y being Element of G2 st y = f . (1_ G1) ; then f .: the carrier of A1 <> {} by A13, A7, FUNCT_1:def_6; then consider A3 being strict Subgroup of G2 such that A51: the carrier of A3 = f .: the carrier of A1 by A9, A26, GROUP_2:52; A52: gr (f .: the carrier of B1) = B3 by A25, Th3; the carrier of (A3 "\/" B3) = the carrier of C3 proof A53: f .: the carrier of B1 c= the carrier of C3 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of B1 or x in the carrier of C3 ) assume A54: x in f .: the carrier of B1 ; ::_thesis: x in the carrier of C3 then reconsider x = x as Element of G2 ; consider y being Element of G1 such that A55: y in the carrier of B1 and A56: x = f . y by A54, FUNCT_2:65; y in A by A55, XBOOLE_0:def_3; then y in gr A by GROUP_4:29; then y in the carrier of (gr A) by STRUCT_0:def_5; then y in the carrier of (A1 "\/" B1) by Th4; hence x in the carrier of C3 by A36, A50, A56, FUNCT_2:35; ::_thesis: verum end; f .: the carrier of A1 c= the carrier of C3 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of A1 or x in the carrier of C3 ) assume A57: x in f .: the carrier of A1 ; ::_thesis: x in the carrier of C3 then reconsider x = x as Element of G2 ; consider y being Element of G1 such that A58: y in the carrier of A1 and A59: x = f . y by A57, FUNCT_2:65; y in A by A58, XBOOLE_0:def_3; then y in gr A by GROUP_4:29; then y in the carrier of (gr A) by STRUCT_0:def_5; then y in the carrier of (A1 "\/" B1) by Th4; hence x in the carrier of C3 by A36, A50, A59, FUNCT_2:35; ::_thesis: verum end; then B c= the carrier of C3 by A53, XBOOLE_1:8; then gr B is Subgroup of C3 by GROUP_4:def_4; then the carrier of (gr B) c= the carrier of C3 by GROUP_2:def_5; hence the carrier of (A3 "\/" B3) c= the carrier of C3 by A51, A25, Th4; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of C3 c= the carrier of (A3 "\/" B3) reconsider AA = (f " the carrier of A3) \/ (f " the carrier of B3) as Subset of G1 ; A60: for g being Element of G1 st g in f " the carrier of (A3 "\/" B3) holds g " in f " the carrier of (A3 "\/" B3) proof let g be Element of G1; ::_thesis: ( g in f " the carrier of (A3 "\/" B3) implies g " in f " the carrier of (A3 "\/" B3) ) assume g in f " the carrier of (A3 "\/" B3) ; ::_thesis: g " in f " the carrier of (A3 "\/" B3) then f . g in the carrier of (A3 "\/" B3) by FUNCT_2:38; then f . g in A3 "\/" B3 by STRUCT_0:def_5; then (f . g) " in A3 "\/" B3 by GROUP_2:51; then f . (g ") in A3 "\/" B3 by GROUP_6:32; then f . (g ") in the carrier of (A3 "\/" B3) by STRUCT_0:def_5; hence g " in f " the carrier of (A3 "\/" B3) by FUNCT_2:38; ::_thesis: verum end; the carrier of B1 c= the carrier of G1 by GROUP_2:def_5; then A61: the carrier of B1 c= f " the carrier of B3 by A25, FUNCT_2:42; the carrier of A1 c= the carrier of G1 by GROUP_2:def_5; then the carrier of A1 c= f " the carrier of A3 by A51, FUNCT_2:42; then A62: A c= AA by A61, XBOOLE_1:13; A63: for g1, g2 being Element of G1 st g1 in f " the carrier of (A3 "\/" B3) & g2 in f " the carrier of (A3 "\/" B3) holds g1 * g2 in f " the carrier of (A3 "\/" B3) proof let g1, g2 be Element of G1; ::_thesis: ( g1 in f " the carrier of (A3 "\/" B3) & g2 in f " the carrier of (A3 "\/" B3) implies g1 * g2 in f " the carrier of (A3 "\/" B3) ) assume that A64: g1 in f " the carrier of (A3 "\/" B3) and A65: g2 in f " the carrier of (A3 "\/" B3) ; ::_thesis: g1 * g2 in f " the carrier of (A3 "\/" B3) f . g2 in the carrier of (A3 "\/" B3) by A65, FUNCT_2:38; then A66: f . g2 in A3 "\/" B3 by STRUCT_0:def_5; f . g1 in the carrier of (A3 "\/" B3) by A64, FUNCT_2:38; then f . g1 in A3 "\/" B3 by STRUCT_0:def_5; then (f . g1) * (f . g2) in A3 "\/" B3 by A66, GROUP_2:50; then f . (g1 * g2) in A3 "\/" B3 by GROUP_6:def_6; then f . (g1 * g2) in the carrier of (A3 "\/" B3) by STRUCT_0:def_5; hence g1 * g2 in f " the carrier of (A3 "\/" B3) by FUNCT_2:38; ::_thesis: verum end; A67: f " the carrier of B3 c= f " the carrier of (A3 "\/" B3) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " the carrier of B3 or x in f " the carrier of (A3 "\/" B3) ) assume A68: x in f " the carrier of B3 ; ::_thesis: x in f " the carrier of (A3 "\/" B3) then f . x in the carrier of B3 by FUNCT_2:38; then A69: f . x in B3 by STRUCT_0:def_5; f . x in the carrier of G2 by A68, FUNCT_2:5; then f . x in A3 "\/" B3 by A69, Th5; then f . x in the carrier of (A3 "\/" B3) by STRUCT_0:def_5; hence x in f " the carrier of (A3 "\/" B3) by A68, FUNCT_2:38; ::_thesis: verum end; 1_ G2 in A3 "\/" B3 by GROUP_2:46; then 1_ G2 in the carrier of (A3 "\/" B3) by STRUCT_0:def_5; then f . (1_ G1) in the carrier of (A3 "\/" B3) by GROUP_6:31; then f " the carrier of (A3 "\/" B3) <> {} by FUNCT_2:38; then consider H being strict Subgroup of G1 such that A70: the carrier of H = f " the carrier of (A3 "\/" B3) by A60, A63, GROUP_2:52; f " the carrier of A3 c= f " the carrier of (A3 "\/" B3) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " the carrier of A3 or x in f " the carrier of (A3 "\/" B3) ) assume A71: x in f " the carrier of A3 ; ::_thesis: x in f " the carrier of (A3 "\/" B3) then f . x in the carrier of A3 by FUNCT_2:38; then A72: f . x in A3 by STRUCT_0:def_5; f . x in the carrier of G2 by A71, FUNCT_2:5; then f . x in A3 "\/" B3 by A72, Th5; then f . x in the carrier of (A3 "\/" B3) by STRUCT_0:def_5; hence x in f " the carrier of (A3 "\/" B3) by A71, FUNCT_2:38; ::_thesis: verum end; then (f " the carrier of A3) \/ (f " the carrier of B3) c= f " the carrier of (A3 "\/" B3) by A67, XBOOLE_1:8; then A c= the carrier of H by A62, A70, XBOOLE_1:1; then gr A is Subgroup of H by GROUP_4:def_4; then the carrier of (gr A) c= the carrier of H by GROUP_2:def_5; then A73: the carrier of C1 c= f " the carrier of (A3 "\/" B3) by A36, A70, Th4; A74: f .: the carrier of C1 c= f .: (f " the carrier of (A3 "\/" B3)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of C1 or x in f .: (f " the carrier of (A3 "\/" B3)) ) assume A75: x in f .: the carrier of C1 ; ::_thesis: x in f .: (f " the carrier of (A3 "\/" B3)) then reconsider x = x as Element of G2 ; ex y being Element of G1 st ( y in the carrier of C1 & x = f . y ) by A75, FUNCT_2:65; hence x in f .: (f " the carrier of (A3 "\/" B3)) by A73, FUNCT_2:35; ::_thesis: verum end; f .: (f " the carrier of (A3 "\/" B3)) c= the carrier of (A3 "\/" B3) by FUNCT_1:75; hence the carrier of C3 c= the carrier of (A3 "\/" B3) by A50, A74, XBOOLE_1:1; ::_thesis: verum end; then gr (f .: the carrier of (A1 "\/" B1)) = A3 "\/" B3 by A36, A50, Th3 .= (gr (f .: the carrier of A1)) "\/" (gr (f .: the carrier of B1)) by A51, A52, Th3 .= ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) by A35, Th22 ; hence (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) by A1, A2, A24, Th22; ::_thesis: verum end; end; hence FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 by VECTSP_8:def_9; ::_thesis: verum 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 proof let G1, G2 be Group; ::_thesis: for f being Homomorphism of G1,G2 st f is one-to-one holds FuncLatt f is Homomorphism of lattice G1, lattice G2 let f be Homomorphism of G1,G2; ::_thesis: ( f is one-to-one implies FuncLatt f is Homomorphism of lattice G1, lattice G2 ) assume f is one-to-one ; ::_thesis: FuncLatt f is Homomorphism of lattice G1, lattice G2 then A1: FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 by Th31; FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 by Th32; hence FuncLatt f is Homomorphism of lattice G1, lattice G2 by A1, VECTSP_8:11; ::_thesis: verum end;