:: Lattice of Subgroups of a Group. Frattini Subgroup :: by Wojciech A. Trybulec :: :: Received August 22, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let D be non empty set ; let F be FinSequence of D; let X be set ; :: original:- redefine funcF - X -> FinSequence of D; coherence F - X is FinSequence of D by FINSEQ_3:86; end; scheme :: GROUP_4:sch 1 MeetSbgEx{ F1() -> Group, P1[ set ] } : ex H being strict Subgroup of F1() st the carrier of H = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st ( A = the carrier of K & P1[K] ) } provided A1: ex H being strict Subgroup of F1() st P1[H] proofend; scheme :: GROUP_4:sch 2 SubgrSep{ F1() -> Group, P1[ set ] } : ex X being set st ( X c= Subgroups F1() & ( for H being strict Subgroup of F1() holds ( H in X iff P1[H] ) ) ) proofend; definition let i be Integer; func @ i -> Element of INT equals :: GROUP_4:def 1 i; coherence i is Element of INT by INT_1:def_2; end; :: deftheorem defines @ GROUP_4:def_1_:_ for i being Integer holds @ i = i; theorem Th1: :: GROUP_4:1 for n being Element of NAT for G being Group for a being Element of G for H being Subgroup of G for h being Element of H st a = h holds a |^ n = h |^ n proofend; theorem :: GROUP_4:2 for i being Integer for G being Group for a being Element of G for H being Subgroup of G for h being Element of H st a = h holds a |^ i = h |^ i proofend; theorem Th3: :: GROUP_4:3 for n being Element of NAT for G being Group for a being Element of G for H being Subgroup of G st a in H holds a |^ n in H proofend; theorem Th4: :: GROUP_4:4 for i being Integer for G being Group for a being Element of G for H being Subgroup of G st a in H holds a |^ i in H proofend; definition let G be non empty multMagma ; let F be FinSequence of the carrier of G; func Product F -> Element of G equals :: GROUP_4:def 2 the multF of G "**" F; correctness coherence the multF of G "**" F is Element of G; ; end; :: deftheorem defines Product GROUP_4:def_2_:_ for G being non empty multMagma for F being FinSequence of the carrier of G holds Product F = the multF of G "**" F; theorem :: GROUP_4:5 for G being non empty unital associative multMagma for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:5; theorem :: GROUP_4:6 for G being non empty unital multMagma for F being FinSequence of the carrier of G for a being Element of G holds Product (F ^ <*a*>) = (Product F) * a by FINSOP_1:4; theorem :: GROUP_4:7 for G being non empty unital associative multMagma for F being FinSequence of the carrier of G for a being Element of G holds Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:6; theorem Th8: :: GROUP_4:8 for G being non empty unital multMagma holds Product (<*> the carrier of G) = 1_ G proofend; theorem :: GROUP_4:9 for G being non empty multMagma for a being Element of G holds Product <*a*> = a by FINSOP_1:11; theorem :: GROUP_4:10 for G being non empty multMagma for a, b being Element of G holds Product <*a,b*> = a * b by FINSOP_1:12; theorem :: GROUP_4:11 for G being Group for a, b, c being Element of G holds ( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) ) proofend; Lm1: now__::_thesis:_for_G_being_Group for_a_being_Element_of_G_holds_Product_(0_|->_a)_=_a_|^_0 let G be Group; ::_thesis: for a being Element of G holds Product (0 |-> a) = a |^ 0 let a be Element of G; ::_thesis: Product (0 |-> a) = a |^ 0 thus Product (0 |-> a) = Product (<*> the carrier of G) .= 1_ G by Th8 .= a |^ 0 by GROUP_1:25 ; ::_thesis: verum end; Lm2: now__::_thesis:_for_G_being_Group for_a_being_Element_of_G for_n_being_Element_of_NAT_st_Product_(n_|->_a)_=_a_|^_n_holds_ Product_((n_+_1)_|->_a)_=_a_|^_(n_+_1) let G be Group; ::_thesis: for a being Element of G for n being Element of NAT st Product (n |-> a) = a |^ n holds Product ((n + 1) |-> a) = a |^ (n + 1) let a be Element of G; ::_thesis: for n being Element of NAT st Product (n |-> a) = a |^ n holds Product ((n + 1) |-> a) = a |^ (n + 1) let n be Element of NAT ; ::_thesis: ( Product (n |-> a) = a |^ n implies Product ((n + 1) |-> a) = a |^ (n + 1) ) assume A1: Product (n |-> a) = a |^ n ; ::_thesis: Product ((n + 1) |-> a) = a |^ (n + 1) thus Product ((n + 1) |-> a) = Product ((n |-> a) ^ <*a*>) by FINSEQ_2:60 .= (Product (n |-> a)) * (Product <*a*>) by FINSOP_1:5 .= (a |^ n) * a by A1, FINSOP_1:11 .= a |^ (n + 1) by GROUP_1:34 ; ::_thesis: verum end; theorem :: GROUP_4:12 for n being Element of NAT for G being Group for a being Element of G holds Product (n |-> a) = a |^ n proofend; theorem :: GROUP_4:13 for G being Group for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F proofend; Lm3: for F1 being FinSequence for y being Element of NAT st y in dom F1 holds ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) proofend; theorem Th14: :: GROUP_4:14 for G being Group for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds Product F1 = (Product F2) " proofend; theorem :: GROUP_4:15 for G being Group for F1, F2 being FinSequence of the carrier of G st G is commutative Group holds for P being Permutation of (dom F1) st F2 = F1 * P holds Product F1 = Product F2 proofend; theorem :: GROUP_4:16 for G being Group for F1, F2 being FinSequence of the carrier of G st G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 holds Product F1 = Product F2 proofend; theorem :: GROUP_4:17 for G being Group for F, F1, F2 being FinSequence of the carrier of G st G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Element of NAT st k in dom F holds F . k = (F1 /. k) * (F2 /. k) ) holds Product F = (Product F1) * (Product F2) proofend; theorem Th18: :: GROUP_4:18 for G being Group for H being Subgroup of G for F being FinSequence of the carrier of G st rng F c= carr H holds Product F in H proofend; definition let G be Group; let I be FinSequence of INT ; let F be FinSequence of the carrier of G; funcF |^ I -> FinSequence of the carrier of G means :Def3: :: GROUP_4:def 3 ( len it = len F & ( for k being Element of NAT st k in dom F holds it . k = (F /. k) |^ (@ (I /. k)) ) ); existence ex b1 being FinSequence of the carrier of G st ( len b1 = len F & ( for k being Element of NAT st k in dom F holds b1 . k = (F /. k) |^ (@ (I /. k)) ) ) proofend; uniqueness for b1, b2 being FinSequence of the carrier of G st len b1 = len F & ( for k being Element of NAT st k in dom F holds b1 . k = (F /. k) |^ (@ (I /. k)) ) & len b2 = len F & ( for k being Element of NAT st k in dom F holds b2 . k = (F /. k) |^ (@ (I /. k)) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines |^ GROUP_4:def_3_:_ for G being Group for I being FinSequence of INT for F, b4 being FinSequence of the carrier of G holds ( b4 = F |^ I iff ( len b4 = len F & ( for k being Element of NAT st k in dom F holds b4 . k = (F /. k) |^ (@ (I /. k)) ) ) ); theorem Th19: :: GROUP_4:19 for G being Group for F1, F2 being FinSequence of the carrier of G for I1, I2 being FinSequence of INT st len F1 = len I1 & len F2 = len I2 holds (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) proofend; theorem Th20: :: GROUP_4:20 for G being Group for H being Subgroup of G for F being FinSequence of the carrier of G for I being FinSequence of INT st rng F c= carr H holds Product (F |^ I) in H proofend; theorem Th21: :: GROUP_4:21 for G being Group holds (<*> the carrier of G) |^ (<*> INT) = {} proofend; theorem Th22: :: GROUP_4:22 for i being Integer for G being Group for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*> proofend; theorem Th23: :: GROUP_4:23 for i, j being Integer for G being Group for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*> proofend; theorem :: GROUP_4:24 for i1, i2, i3 being Integer for G being Group for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*> proofend; theorem :: GROUP_4:25 for G being Group for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 1)) = F proofend; theorem :: GROUP_4:26 for G being Group for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G) proofend; theorem :: GROUP_4:27 for n being Element of NAT for G being Group for I being FinSequence of INT st len I = n holds (n |-> (1_ G)) |^ I = n |-> (1_ G) proofend; definition let G be Group; let A be Subset of G; func gr A -> strict Subgroup of G means :Def4: :: GROUP_4:def 4 ( A c= the carrier of it & ( for H being strict Subgroup of G st A c= the carrier of H holds it is Subgroup of H ) ); existence ex b1 being strict Subgroup of G st ( A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds b1 is Subgroup of H ) ) proofend; uniqueness for b1, b2 being strict Subgroup of G st A c= the carrier of b1 & ( for H being strict Subgroup of G st A c= the carrier of H holds b1 is Subgroup of H ) & A c= the carrier of b2 & ( for H being strict Subgroup of G st A c= the carrier of H holds b2 is Subgroup of H ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines gr GROUP_4:def_4_:_ for G being Group for A being Subset of G for b3 being strict Subgroup of G holds ( b3 = gr A iff ( A c= the carrier of b3 & ( for H being strict Subgroup of G st A c= the carrier of H holds b3 is Subgroup of H ) ) ); theorem Th28: :: GROUP_4:28 for G being Group for a being Element of G for A being Subset of G holds ( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st ( len F = len I & rng F c= A & Product (F |^ I) = a ) ) proofend; theorem Th29: :: GROUP_4:29 for G being Group for a being Element of G for A being Subset of G st a in A holds a in gr A proofend; theorem :: GROUP_4:30 for G being Group holds gr ({} the carrier of G) = (1). G proofend; theorem Th31: :: GROUP_4:31 for G being Group for H being strict Subgroup of G holds gr (carr H) = H proofend; theorem Th32: :: GROUP_4:32 for G being Group for A, B being Subset of G st A c= B holds gr A is Subgroup of gr B proofend; theorem :: GROUP_4:33 for G being Group for A, B being Subset of G holds gr (A /\ B) is Subgroup of (gr A) /\ (gr B) proofend; theorem Th34: :: GROUP_4:34 for G being Group for A being Subset of G holds the carrier of (gr A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st ( B = the carrier of H & A c= carr H ) } proofend; theorem Th35: :: GROUP_4:35 for G being Group for A being Subset of G holds gr A = gr (A \ {(1_ G)}) proofend; definition let G be Group; let a be Element of G; attra is generating means :Def5: :: GROUP_4:def 5 ex A being Subset of G st ( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ); end; :: deftheorem Def5 defines generating GROUP_4:def_5_:_ for G being Group for a being Element of G holds ( a is generating iff ex A being Subset of G st ( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ) ); theorem :: GROUP_4:36 for G being Group holds not 1_ G is generating proofend; definition let G be Group; let H be Subgroup of G; attrH is maximal means :Def6: :: GROUP_4:def 6 ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds K = multMagma(# the carrier of G, the multF of G #) ) ); end; :: deftheorem Def6 defines maximal GROUP_4:def_6_:_ for G being Group for H being Subgroup of G holds ( H is maximal iff ( multMagma(# the carrier of H, the multF of H #) <> multMagma(# the carrier of G, the multF of G #) & ( for K being strict Subgroup of G st multMagma(# the carrier of H, the multF of H #) <> K & H is Subgroup of K holds K = multMagma(# the carrier of G, the multF of G #) ) ) ); theorem Th37: :: GROUP_4:37 for G being strict Group for H being strict Subgroup of G for a being Element of G st H is maximal & not a in H holds gr ((carr H) \/ {a}) = G proofend; :: :: Frattini subgroup. :: definition let G be Group; func Phi G -> strict Subgroup of G means :Def7: :: GROUP_4:def 7 the carrier of it = meet { A where A is Subset of G : ex H being strict Subgroup of G st ( A = the carrier of H & H is maximal ) } if ex H being strict Subgroup of G st H is maximal otherwise it = multMagma(# the carrier of G, the multF of G #); existence ( ( ex H being strict Subgroup of G st H is maximal implies ex b1 being strict Subgroup of G st the carrier of b1 = meet { A where A is Subset of G : ex H being strict Subgroup of G st ( A = the carrier of H & H is maximal ) } ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ex b1 being strict Subgroup of G st b1 = multMagma(# the carrier of G, the multF of G #) ) ) proofend; uniqueness for b1, b2 being strict Subgroup of G holds ( ( ex H being strict Subgroup of G st H is maximal & the carrier of b1 = meet { A where A is Subset of G : ex H being strict Subgroup of G st ( A = the carrier of H & H is maximal ) } & the carrier of b2 = meet { A where A is Subset of G : ex H being strict Subgroup of G st ( A = the carrier of H & H is maximal ) } implies b1 = b2 ) & ( ( for H being strict Subgroup of G holds not H is maximal ) & b1 = multMagma(# the carrier of G, the multF of G #) & b2 = multMagma(# the carrier of G, the multF of G #) implies b1 = b2 ) ) by GROUP_2:59; correctness consistency for b1 being strict Subgroup of G holds verum; ; end; :: deftheorem Def7 defines Phi GROUP_4:def_7_:_ for G being Group for b2 being strict Subgroup of G holds ( ( ex H being strict Subgroup of G st H is maximal implies ( b2 = Phi G iff the carrier of b2 = meet { A where A is Subset of G : ex H being strict Subgroup of G st ( A = the carrier of H & H is maximal ) } ) ) & ( ( for H being strict Subgroup of G holds not H is maximal ) implies ( b2 = Phi G iff b2 = multMagma(# the carrier of G, the multF of G #) ) ) ); theorem Th38: :: GROUP_4:38 for G being Group for a being Element of G for G being Group st ex H being strict Subgroup of G st H is maximal holds ( a in Phi G iff for H being strict Subgroup of G st H is maximal holds a in H ) proofend; theorem :: GROUP_4:39 for G being Group for a being Element of G st ( for H being strict Subgroup of G holds not H is maximal ) holds a in Phi G proofend; theorem Th40: :: GROUP_4:40 for G being Group for H being strict Subgroup of G st H is maximal holds Phi G is Subgroup of H proofend; theorem Th41: :: GROUP_4:41 for G being strict Group holds the carrier of (Phi G) = { a where a is Element of G : not a is generating } proofend; theorem :: GROUP_4:42 for G being strict Group for a being Element of G holds ( a in Phi G iff not a is generating ) proofend; definition let G be Group; let H1, H2 be Subgroup of G; funcH1 * H2 -> Subset of G equals :: GROUP_4:def 8 (carr H1) * (carr H2); correctness coherence (carr H1) * (carr H2) is Subset of G; ; end; :: deftheorem defines * GROUP_4:def_8_:_ for G being Group for H1, H2 being Subgroup of G holds H1 * H2 = (carr H1) * (carr H2); theorem :: GROUP_4:43 for G being Group for H1, H2 being Subgroup of G holds ( H1 * H2 = (carr H1) * (carr H2) & H1 * H2 = H1 * (carr H2) & H1 * H2 = (carr H1) * H2 ) ; theorem :: GROUP_4:44 for G being Group for H1, H2, H3 being Subgroup of G holds (H1 * H2) * H3 = H1 * (H2 * H3) proofend; theorem :: GROUP_4:45 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds (a * H1) * H2 = a * (H1 * H2) proofend; theorem :: GROUP_4:46 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds (H1 * H2) * a = H1 * (H2 * a) proofend; theorem :: GROUP_4:47 for G being Group for A being Subset of G for H1, H2 being Subgroup of G holds (A * H1) * H2 = A * (H1 * H2) proofend; theorem :: GROUP_4:48 for G being Group for A being Subset of G for H1, H2 being Subgroup of G holds (H1 * H2) * A = H1 * (H2 * A) proofend; definition let G be Group; let H1, H2 be Subgroup of G; funcH1 "\/" H2 -> strict Subgroup of G equals :: GROUP_4:def 9 gr ((carr H1) \/ (carr H2)); correctness coherence gr ((carr H1) \/ (carr H2)) is strict Subgroup of G; ; end; :: deftheorem defines "\/" GROUP_4:def_9_:_ for G being Group for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr ((carr H1) \/ (carr H2)); theorem :: GROUP_4:49 for G being Group for a being Element of G for H1, H2 being Subgroup of G holds ( a in H1 "\/" H2 iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st ( len F = len I & rng F c= (carr H1) \/ (carr H2) & a = Product (F |^ I) ) ) by Th28; theorem :: GROUP_4:50 for G being Group for H1, H2 being Subgroup of G holds H1 "\/" H2 = gr (H1 * H2) proofend; theorem Th51: :: GROUP_4:51 for G being Group for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds the carrier of (H1 "\/" H2) = H1 * H2 proofend; theorem :: GROUP_4:52 for G being Group for H1, H2 being Subgroup of G st G is commutative Group holds the carrier of (H1 "\/" H2) = H1 * H2 proofend; theorem Th53: :: GROUP_4:53 for G being Group for N1, N2 being strict normal Subgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2 proofend; theorem :: GROUP_4:54 for G being Group for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G proofend; theorem :: GROUP_4:55 for G being Group for H being strict Subgroup of G holds H "\/" H = H by Th31; theorem :: GROUP_4:56 for G being Group for H1, H2 being Subgroup of G holds H1 "\/" H2 = H2 "\/" H1 ; Lm4: for G being Group for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2 proofend; Lm5: for G being Group for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) proofend; theorem Th57: :: GROUP_4:57 for G being Group for H1, H2, H3 being Subgroup of G holds (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3) proofend; theorem :: GROUP_4:58 for G being Group for H being strict Subgroup of G holds ( ((1). G) "\/" H = H & H "\/" ((1). G) = H ) proofend; theorem Th59: :: GROUP_4:59 for G being Group for H being Subgroup of G holds ( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G ) proofend; theorem Th60: :: GROUP_4:60 for G being Group for H1, H2 being Subgroup of G holds ( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 ) proofend; theorem Th61: :: GROUP_4:61 for G being Group for H1 being Subgroup of G for H2 being strict Subgroup of G holds ( H1 is Subgroup of H2 iff H1 "\/" H2 = H2 ) proofend; theorem :: GROUP_4:62 for G being Group for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 holds H1 is Subgroup of H2 "\/" H3 proofend; theorem :: GROUP_4:63 for G being Group for H1, H2 being Subgroup of G for H3 being strict Subgroup of G st H1 is Subgroup of H3 & H2 is Subgroup of H3 holds H1 "\/" H2 is Subgroup of H3 proofend; theorem :: GROUP_4:64 for G being Group for H1 being Subgroup of G for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds H1 "\/" H3 is Subgroup of H2 "\/" H3 proofend; theorem :: GROUP_4:65 for G being Group for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 "\/" H2 proofend; theorem Th66: :: GROUP_4:66 for G being Group for H1 being Subgroup of G for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2 proofend; theorem Th67: :: GROUP_4:67 for G being Group for H2 being Subgroup of G for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1 proofend; theorem :: GROUP_4:68 for G being Group for H1, H2 being strict Subgroup of G holds ( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 ) proofend; definition let G be Group; func SubJoin G -> BinOp of (Subgroups G) means :Def10: :: GROUP_4:def 10 for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 "\/" H2; existence ex b1 being BinOp of (Subgroups G) st for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 "\/" H2 proofend; uniqueness for b1, b2 being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 "\/" H2 ) & ( for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 "\/" H2 ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines SubJoin GROUP_4:def_10_:_ for G being Group for b2 being BinOp of (Subgroups G) holds ( b2 = SubJoin G iff for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 "\/" H2 ); definition let G be Group; func SubMeet G -> BinOp of (Subgroups G) means :Def11: :: GROUP_4:def 11 for H1, H2 being strict Subgroup of G holds it . (H1,H2) = H1 /\ H2; existence ex b1 being BinOp of (Subgroups G) st for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 /\ H2 proofend; uniqueness for b1, b2 being BinOp of (Subgroups G) st ( for H1, H2 being strict Subgroup of G holds b1 . (H1,H2) = H1 /\ H2 ) & ( for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 /\ H2 ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines SubMeet GROUP_4:def_11_:_ for G being Group for b2 being BinOp of (Subgroups G) holds ( b2 = SubMeet G iff for H1, H2 being strict Subgroup of G holds b2 . (H1,H2) = H1 /\ H2 ); Lm6: for G being Group holds ( 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 ) proofend; definition let G be Group; func lattice G -> strict Lattice equals :: GROUP_4:def 12 LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); coherence LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #) is strict Lattice by Lm6; end; :: deftheorem defines lattice GROUP_4:def_12_:_ for G being Group holds lattice G = LattStr(# (Subgroups G),(SubJoin G),(SubMeet G) #); theorem :: GROUP_4:69 for G being Group holds the carrier of (lattice G) = Subgroups G ; theorem :: GROUP_4:70 for G being Group holds the L_join of (lattice G) = SubJoin G ; theorem :: GROUP_4:71 for G being Group holds the L_meet of (lattice G) = SubMeet G ; registration let G be Group; cluster lattice G -> strict lower-bounded upper-bounded ; coherence ( lattice G is lower-bounded & lattice G is upper-bounded ) by Lm6; end; theorem :: GROUP_4:72 for G being Group holds Bottom (lattice G) = (1). G proofend; theorem :: GROUP_4:73 for G being Group holds Top (lattice G) = (Omega). G proofend;