Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Lattice of Subgroups of a Group. Frattini Subgroup

**by****Wojciech A. Trybulec**- Received August 22, 1990
- MML identifier: GROUP_4

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, ARYTM_1, REALSET1, GROUP_2, SETFAM_1, GROUP_1, BOOLE, RELAT_1, INT_1, GROUP_3, QC_LANG1, ABSVALUE, VECTSP_1, FINSOP_1, BINOP_1, SETWISEO, FUNCT_1, FINSEQ_2, FUNCT_2, RLSUB_1, TARSKI, LATTICES, NAT_1, SUBSET_1, RLSUB_2, GROUP_4, CARD_3, FINSEQ_4, ORDINAL2, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, FINSOP_1, ORDINAL1, ORDINAL2, INT_1, SETWISEO, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, GROUP_2, GROUP_3, LATTICES, GROUP_1, DOMAIN_1, NAT_1; constructors FINSOP_1, SETWISEO, FUNCSDOM, FINSEQ_3, GROUP_3, LATTICES, DOMAIN_1, NAT_1, FINSEQ_4, MEMBERED, XBOOLE_0, ORDINAL2, ORDINAL1; clusters SUBSET_1, FINSEQ_1, GROUP_3, INT_1, LATTICES, GROUP_1, RELSET_1, STRUCT_0, RLSUB_2, GROUP_2, XREAL_0, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS, ARYTM_3; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin definition let D be non empty set; let F be FinSequence of D; let X be set; redefine func F - X -> FinSequence of D; end; scheme MeetSbgEx{G() -> Group, P[set]}: ex H being strict Subgroup of G() st the carrier of H = meet{A where A is Subset of G() : ex K being strict Subgroup of G() st A = the carrier of K & P[K]} provided ex H being strict Subgroup of G() st P[H]; reserve x,y,y1,y2,X,Y for set, k,l,m,n for Nat, i,i1,i2,i3,j for Integer, G for Group, a,b,c,d for Element of G, A,B,C for Subset of G, H,H1,H2,H3 for Subgroup of G, h for Element of H, F,F1,F2 for FinSequence of the carrier of G, I,I1,I2 for FinSequence of INT; scheme SubgrSep{G() -> Group,P[set]}: ex X st X c= Subgroups G() & for H being strict Subgroup of G() holds H in X iff P[H]; definition let i; canceled; func @i -> Element of INT equals :: GROUP_4:def 2 i; end; canceled 2; theorem :: GROUP_4:3 a = h implies a |^ n = h |^ n; theorem :: GROUP_4:4 a = h implies a |^ i = h |^ i; theorem :: GROUP_4:5 a in H implies a |^ n in H; theorem :: GROUP_4:6 a in H implies a |^ i in H; definition let G be non empty HGrStr; let F be FinSequence of the carrier of G; func Product F -> Element of G equals :: GROUP_4:def 3 (the mult of G) "**" F; end; canceled; theorem :: GROUP_4:8 for G being associative unital (non empty HGrStr), F1,F2 being FinSequence of the carrier of G holds Product(F1 ^ F2) = Product(F1) * Product(F2); theorem :: GROUP_4:9 for G being unital (non empty HGrStr), F being FinSequence of the carrier of G, a being Element of G holds Product(F ^ <* a *>) = Product(F) * a; theorem :: GROUP_4:10 for G being associative unital (non empty HGrStr), F being FinSequence of the carrier of G, a being Element of G holds Product(<* a *> ^ F) = a * Product(F); theorem :: GROUP_4:11 for G being unital (non empty HGrStr) holds Product <*> the carrier of G = 1.G; theorem :: GROUP_4:12 for G being non empty HGrStr, a being Element of G holds Product<* a *> = a; theorem :: GROUP_4:13 for G being non empty HGrStr, a,b being Element of G holds Product<* a,b *> = a * b; theorem :: GROUP_4:14 Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c); theorem :: GROUP_4:15 Product(n |-> a) = a |^ n; theorem :: GROUP_4:16 Product(F - {1.G}) = Product(F); theorem :: GROUP_4:17 len F1 = len F2 & (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") implies Product(F1) = Product(F2)"; theorem :: GROUP_4:18 G is commutative Group implies for P being Permutation of dom F1 st F2 = F1 * P holds Product(F1) = Product(F2); theorem :: GROUP_4:19 G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 implies Product(F1) = Product(F2); theorem :: GROUP_4:20 G is commutative Group & len F = len F1 & len F = len F2 & (for k st k in dom F holds F.k = (F1/.k) * (F2/.k)) implies Product(F) = Product(F1) * Product(F2); theorem :: GROUP_4:21 rng F c= carr H implies Product(F) in H; definition let G,I,F; func F |^ I -> FinSequence of the carrier of G means :: GROUP_4:def 4 len it = len F & for k st k in dom F holds it.k = (F/.k) |^ @(I/.k); end; canceled 3; theorem :: GROUP_4:25 len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2); theorem :: GROUP_4:26 rng F c= carr H implies Product(F |^ I) in H; theorem :: GROUP_4:27 (<*> the carrier of G) |^ (<*> INT) = {}; theorem :: GROUP_4:28 <* a *> |^ <* @i *> = <* a |^ i *>; theorem :: GROUP_4:29 <* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>; theorem :: GROUP_4:30 <* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>; theorem :: GROUP_4:31 F |^ (len F |-> @(1)) = F; theorem :: GROUP_4:32 F |^ (len F |-> @(0)) = len F |-> 1.G; theorem :: GROUP_4:33 len I = n implies (n |-> 1.G) |^ I = n |-> 1.G; definition let G,A; func gr A -> strict Subgroup of G means :: GROUP_4:def 5 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); end; canceled 3; theorem :: GROUP_4:37 a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a; theorem :: GROUP_4:38 a in A implies a in gr A; theorem :: GROUP_4:39 gr {} the carrier of G = (1).G; theorem :: GROUP_4:40 for H being strict Subgroup of G holds gr carr H = H; theorem :: GROUP_4:41 A c= B implies gr A is Subgroup of gr B; theorem :: GROUP_4:42 gr(A /\ B) is Subgroup of gr A /\ gr B; theorem :: GROUP_4:43 the carrier of gr A = meet{B : ex H being strict Subgroup of G st B = the carrier of H & A c= carr H}; theorem :: GROUP_4:44 gr A = gr(A \ {1.G}); definition let G,a; attr a is generating means :: GROUP_4:def 6 not for A st gr A = the HGrStr of G holds gr(A \ {a}) = the HGrStr of G; end; canceled; theorem :: GROUP_4:46 1.G is non generating; definition let G, H; attr H is maximal means :: GROUP_4:def 7 the HGrStr of H <> the HGrStr of G & for K being strict Subgroup of G st the HGrStr of H <> K & H is Subgroup of K holds K = the HGrStr of G; end; canceled; theorem :: GROUP_4:48 for G being strict Group, H being strict Subgroup of G, a being Element of G holds H is maximal & not a in H implies gr(carr H \/ {a}) = G; :: :: Frattini subgroup. :: definition let G be Group; func Phi(G) -> strict Subgroup of G means :: GROUP_4:def 8 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 = the HGrStr of G; end; canceled 3; theorem :: GROUP_4:52 for G being Group holds (ex H being strict Subgroup of G st H is maximal) implies (a in Phi(G) iff for H being strict Subgroup of G st H is maximal holds a in H); theorem :: GROUP_4:53 for G being Group, a being Element of G holds (for H being strict Subgroup of G holds H is not maximal) implies a in Phi(G); theorem :: GROUP_4:54 for G being Group, H being strict Subgroup of G holds H is maximal implies Phi(G) is Subgroup of H; theorem :: GROUP_4:55 for G being strict Group holds the carrier of Phi(G) = {a where a is Element of G: a is non generating}; theorem :: GROUP_4:56 for G being strict Group, a being Element of G holds a in Phi(G) iff a is non generating; definition let G,H1,H2; func H1 * H2 -> Subset of G equals :: GROUP_4:def 9 carr H1 * carr H2; end; theorem :: GROUP_4:57 H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 & H1 * H2 = carr H1 * H2; theorem :: GROUP_4:58 H * H = carr H; theorem :: GROUP_4:59 H1 * H2 * H3 = H1 * (H2 * H3); theorem :: GROUP_4:60 a * H1 * H2 = a * (H1 * H2); theorem :: GROUP_4:61 H1 * H2 * a = H1 * (H2 * a); theorem :: GROUP_4:62 A * H1 * H2 = A * (H1 * H2); theorem :: GROUP_4:63 H1 * H2 * A = H1 * (H2 * A); theorem :: GROUP_4:64 for N1,N2 being strict normal Subgroup of G holds N1 * N2 = N2 * N1; theorem :: GROUP_4:65 G is commutative Group implies H1 * H2 = H2 * H1; definition let G,H1,H2; func H1 "\/" H2 -> strict Subgroup of G equals :: GROUP_4:def 10 gr(carr H1 \/ carr H2); end; canceled; theorem :: GROUP_4:67 a in H1 "\/" H2 iff ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I); theorem :: GROUP_4:68 H1 "\/" H2 = gr(H1 * H2); theorem :: GROUP_4:69 H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2; theorem :: GROUP_4:70 G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2; theorem :: GROUP_4:71 for N1,N2 being strict normal Subgroup of G holds the carrier of N1 "\/" N2 = N1 * N2; theorem :: GROUP_4:72 for N1,N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G; theorem :: GROUP_4:73 for H being strict Subgroup of G holds H "\/" H = H; theorem :: GROUP_4:74 H1 "\/" H2 = H2 "\/" H1; theorem :: GROUP_4:75 H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3); theorem :: GROUP_4:76 for H being strict Subgroup of G holds (1).G "\/" H = H & H "\/" (1).G = H; theorem :: GROUP_4:77 (Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G; theorem :: GROUP_4:78 H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2; theorem :: GROUP_4:79 for H2 being strict Subgroup of G holds H1 is Subgroup of H2 iff H1 "\/" H2 = H2; theorem :: GROUP_4:80 H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3; theorem :: GROUP_4:81 for H3 being strict Subgroup of G holds H1 is Subgroup of H3 & H2 is Subgroup of H3 implies H1 "\/" H2 is Subgroup of H3; theorem :: GROUP_4:82 for H3,H2 being strict Subgroup of G holds H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3; theorem :: GROUP_4:83 H1 /\ H2 is Subgroup of H1 "\/" H2; theorem :: GROUP_4:84 for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2; theorem :: GROUP_4:85 for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1; theorem :: GROUP_4:86 for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1 ; reserve S1,S2 for Element of Subgroups G; definition let G; func SubJoin G -> BinOp of Subgroups G means :: GROUP_4:def 11 for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 "\/" H2; end; definition let G; func SubMeet G -> BinOp of Subgroups G means :: GROUP_4:def 12 for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 /\ H2; end; definition let G be Group; func lattice G -> strict Lattice equals :: GROUP_4:def 13 LattStr (# Subgroups G, SubJoin G, SubMeet G #); end; canceled 5; theorem :: GROUP_4:92 for G being Group holds the carrier of lattice G = Subgroups G; theorem :: GROUP_4:93 for G being Group holds the L_join of lattice G = SubJoin G; theorem :: GROUP_4:94 for G being Group holds the L_meet of lattice G = SubMeet G; definition let G be Group; cluster lattice G -> lower-bounded upper-bounded; end; canceled 3; theorem :: GROUP_4:98 for G being Group holds Bottom lattice G = (1).G; theorem :: GROUP_4:99 for G being Group holds Top lattice G = (Omega).G; :: :: Auxiliary theorems. :: reserve k, l, m, n for natural number; theorem :: GROUP_4:100 n mod 2 = 0 or n mod 2 = 1; theorem :: GROUP_4:101 for k, n being Nat holds (k * n) mod k = 0; theorem :: GROUP_4:102 k > 1 implies 1 mod k = 1; theorem :: GROUP_4:103 k mod n = 0 & l = k - m * n implies l mod n = 0; reserve k, n, l, m for Nat; theorem :: GROUP_4:104 n <> 0 & k mod n = 0 & l < n implies k + l mod n = l; theorem :: GROUP_4:105 k mod n = 0 implies k + l mod n = l mod n; theorem :: GROUP_4:106 n <> 0 & k mod n = 0 implies (k + l) div n = (k div n) + (l div n); theorem :: GROUP_4:107 k <> 0 implies (k * n) div k = n;

Back to top