let G be Group; :: thesis: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice )
set L = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #);
A1: now :: thesis: for A, B being Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #)
for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "\/" B = H1 "\/" H2
let A, B be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); :: thesis: for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "\/" B = H1 "\/" H2
let H1, H2 be strict Subgroup of G; :: thesis: ( A = H1 & B = H2 implies A "\/" B = H1 "\/" H2 )
assume A2: ( A = H1 & B = H2 ) ; :: thesis: A "\/" B = H1 "\/" H2
thus A "\/" B = (SubJoin G) . (A,B) by LATTICES:def 1
.= H1 "\/" H2 by A2, Def10 ; :: thesis: verum
end;
A3: now :: thesis: for A, B being Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #)
for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "/\" B = H1 /\ H2
let A, B be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); :: thesis: for H1, H2 being strict Subgroup of G st A = H1 & B = H2 holds
A "/\" B = H1 /\ H2
let H1, H2 be strict Subgroup of G; :: thesis: ( A = H1 & B = H2 implies A "/\" B = H1 /\ H2 )
assume A4: ( A = H1 & B = H2 ) ; :: thesis: A "/\" B = H1 /\ H2
thus A "/\" B = (SubMeet G) . (A,B) by LATTICES:def 2
.= H1 /\ H2 by A4, Def11 ; :: thesis: verum
end;
now :: thesis: for A, B, C being Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) holds
( A "\/" B = B "\/" A & (A "\/" B) "\/" C = A "\/" (B "\/" C) & (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
let A, B, C be Element of LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); :: thesis: ( A "\/" B = B "\/" A & (A "\/" B) "\/" C = A "\/" (B "\/" C) & (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
reconsider H1 = A, H2 = B, H3 = C as strict Subgroup of G by GROUP_3:def 1;
A5: H2 "\/" H3 = B "\/" C by A1;
thus A "\/" B = H1 "\/" H2 by A1
.= H2 "\/" H1
.= B "\/" A by A1 ; :: thesis: ( (A "\/" B) "\/" C = A "\/" (B "\/" C) & (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A6: H1 "\/" H2 = A "\/" B by A1;
hence (A "\/" B) "\/" C = (H1 "\/" H2) "\/" H3 by A1
.= H1 "\/" (H2 "\/" H3) by Th57
.= A "\/" (B "\/" C) by A1, A5 ;
:: thesis: ( (A "/\" B) "\/" B = B & A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A7: H1 /\ H2 = A "/\" B by A3;
hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A1
.= B by Th66 ;
:: thesis: ( A "/\" B = B "/\" A & (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
A8: H2 /\ H3 = B "/\" C by A3;
thus A "/\" B = H2 /\ H1 by A3
.= B "/\" A by A3 ; :: thesis: ( (A "/\" B) "/\" C = A "/\" (B "/\" C) & A "/\" (A "\/" B) = A )
thus (A "/\" B) "/\" C = (H1 /\ H2) /\ H3 by A3, A7
.= H1 /\ (H2 /\ H3) by GROUP_2:84
.= A "/\" (B "/\" C) by A3, A8 ; :: thesis: A "/\" (A "\/" B) = A
thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A3, A6
.= A by Th67 ; :: thesis: verum
end;
then A9: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-commutative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-associative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-absorbing & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-commutative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is meet-associative & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is join-absorbing ) by LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is Lattice ; :: thesis: ( LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice & LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice )
reconsider L = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) as Lattice by A9;
reconsider E = (1). G as Element of L by GROUP_3:def 1;
now :: thesis: for A being Element of L holds
( E "/\" A = E & A "/\" E = E )
let A be Element of L; :: thesis: ( E "/\" A = E & A "/\" E = E )
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus E "/\" A = ((1). G) /\ H by A3
.= E by GROUP_2:85 ; :: thesis: A "/\" E = E
hence A "/\" E = E ; :: thesis: verum
end;
hence LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 0_Lattice by LATTICES:def 13; :: thesis: LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice
reconsider F = (Omega). G as Element of L by GROUP_3:def 1;
now :: thesis: for A being Element of L holds
( F "\/" A = F & A "\/" F = F )
let A be Element of L; :: thesis: ( F "\/" A = F & A "\/" F = F )
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus F "\/" A = ((Omega). G) "\/" H by A1
.= F by Th59 ; :: thesis: A "\/" F = F
hence A "\/" F = F ; :: thesis: verum
end;
hence LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is 1_Lattice by LATTICES:def 14; :: thesis: verum