:: 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;