### The Mizar article:

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

**by****Wojciech A. Trybulec**

- Received August 22, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: GROUP_4
- [ 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; definitions TARSKI, XBOOLE_0; theorems AXIOMS, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSOP_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_2, GROUP_3, INT_1, LATTICES, NAT_1, ORDERS_1, REAL_1, RLSUB_2, RLVECT_1, SETFAM_1, SUBSET_1, TARSKI, ZFMISC_1, VECTSP_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes BINOP_1, DOMAIN_1, FINSEQ_1, FINSEQ_2, NAT_1, ORDERS_2, XBOOLE_0; 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; coherence by FINSEQ_3:93; 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 A1: ex H being strict Subgroup of G() st P[H] proof set X = {A where A is Subset of G(): ex K being strict Subgroup of G() st A = the carrier of K & P[K]}; consider T being strict Subgroup of G() such that A2: P[T] by A1; carr T = the carrier of T by GROUP_2:def 9; then A3: carr T in X by A2; then reconsider Y = meet X as Subset of G() by SETFAM_1:8; now let Z be set; assume Z in X; then consider A being Subset of G() such that A4: Z = A and A5: ex K being strict Subgroup of G() st A = the carrier of K & P[K]; consider H being Subgroup of G() such that A6: A = the carrier of H & P[H] by A5; 1.G() in H by GROUP_2:55; hence 1.G() in Z by A4,A6,RLVECT_1:def 1; end; then A7: Y <> {} by A3,SETFAM_1:def 1; A8: now let a,b be Element of G(); assume A9: a in Y & b in Y; now let Z be set; assume A10: Z in X; then consider A being Subset of G() such that A11: A = Z and A12: ex H being strict Subgroup of G() st A = the carrier of H & P[H]; consider H being Subgroup of G() such that A13: A = the carrier of H & P[H] by A12; a in the carrier of H & b in the carrier of H by A9,A10,A11,A13,SETFAM_1:def 1; then a in H & b in H by RLVECT_1:def 1; then a * b in H by GROUP_2:59; hence a * b in Z by A11,A13,RLVECT_1:def 1; end; hence a * b in Y by A3,SETFAM_1:def 1; end; now let a be Element of G(); assume A14: a in Y; now let Z be set; assume A15: Z in X; then consider A being Subset of G() such that A16: A = Z and A17: ex H being strict Subgroup of G() st A = the carrier of H & P[H]; consider H being Subgroup of G() such that A18: A = the carrier of H & P[H] by A17; a in the carrier of H by A14,A15,A16,A18,SETFAM_1:def 1; then a in H by RLVECT_1:def 1; then a" in H by GROUP_2:60; hence a" in Z by A16,A18,RLVECT_1:def 1; end; hence a" in Y by A3,SETFAM_1:def 1; end; hence thesis by A7,A8,GROUP_2:61; end; 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] proof defpred R[set] means ex H being Subgroup of G() st $1 = H & P[H]; consider X such that A1: x in X iff x in Subgroups G() & R[x] from Separation; take X; thus X c= Subgroups G() proof let x; assume x in X; hence x in Subgroups G() by A1; end; let H be strict Subgroup of G(); thus H in X implies P[H] proof assume H in X; then ex H1 being Subgroup of G() st H = H1 & P[H1] by A1; hence thesis; end; assume A2: P[H]; H in Subgroups G() by GROUP_3:def 1; hence thesis by A1,A2; end; definition let i; canceled; func @i -> Element of INT equals :Def2: i; coherence by INT_1:12; end; canceled 2; theorem Th3: a = h implies a |^ n = h |^ n proof assume A1: a = h; defpred P[Nat] means a |^ $1 = h |^ $1; a |^ 0 = 1.G by GROUP_1:43 .= 1.H by GROUP_2:53 .= h |^ 0 by GROUP_1:43; then A2: P[0]; A3: now let n; assume A4: P[n]; a |^ (n + 1) = a |^ n * a by GROUP_1:49 .= h |^ n * h by A1,A4,GROUP_2:52 .= h |^ (n + 1) by GROUP_1:49; hence P[n+1]; end; for n holds P[n] from Ind(A2,A3); hence thesis; end; theorem a = h implies a |^ i = h |^ i proof assume A1: a = h; now per cases; suppose A2: i >= 0; hence a |^ i = a |^ abs( i ) by GROUP_1:55 .= h |^ abs( i ) by A1,Th3 .= h |^ i by A2,GROUP_1:55; suppose A3: i < 0; A4: a |^ abs( i ) = h |^ abs( i ) by A1,Th3; thus a |^ i = (a |^ abs( i ))" by A3,GROUP_1:56 .= (h |^ abs( i ))" by A4,GROUP_2:57 .= h |^ i by A3,GROUP_1:56; end; hence thesis; end; theorem Th5: a in H implies a |^ n in H proof assume A1: a in H; defpred P[Nat] means a |^ $1 in H; a |^ 0 = 1.G by GROUP_1:43; then A2: P[0] by GROUP_2:55; A3: now let n; assume A4: P[n]; a |^ (n + 1) = a |^ n * a by GROUP_1:49; hence P[n+1] by A1,A4,GROUP_2:59; end; for n holds P[n] from Ind(A2,A3); hence thesis; end; theorem Th6: a in H implies a |^ i in H proof assume A1: a in H; now per cases; suppose i >= 0; then a |^ i = a |^ abs( i ) by GROUP_1:55; hence thesis by A1,Th5; suppose i < 0; then a |^ i = (a |^ abs( i ))" & a |^ abs( i ) in H by A1,Th5,GROUP_1:56; hence thesis by GROUP_2:60; end; hence thesis; end; definition let G be non empty HGrStr; let F be FinSequence of the carrier of G; func Product F -> Element of G equals :Def3: (the mult of G) "**" F; correctness; end; canceled; theorem Th8: 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) proof let G be associative unital (non empty HGrStr), F1,F2 be FinSequence of the carrier of G; set g = the mult of G; A1: g is associative & g has_a_unity by GROUP_1:31,34; thus Product(F1 ^ F2) = g "**" (F1 ^ F2) by Def3 .= g.(g "**" F1,g "**" F2)by A1,FINSOP_1:6 .= g.(Product(F1),g "**" F2) by Def3 .= g.(Product F1,Product F2) by Def3 .= Product F1 * Product F2 by VECTSP_1:def 10; end; theorem Th9: 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 proof let G be unital (non empty HGrStr), F be FinSequence of the carrier of G, a be Element of G; set g = the mult of G; A1: g has_a_unity by GROUP_1:34; thus Product(F ^ <* a *>) = g "**" (F ^ <* a *>) by Def3 .= g.(g "**" F,a) by A1,FINSOP_1:5 .= (g "**" F) * a by VECTSP_1:def 10 .= Product F * a by Def3; end; theorem Th10: 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) proof let G be associative unital (non empty HGrStr), F be FinSequence of the carrier of G, a be Element of G; set g = the mult of G; A1: g is associative & g has_a_unity by GROUP_1:31,34; thus Product(<* a *> ^ F) = g "**" (<* a *> ^ F) by Def3 .= g.(a,g "**" F) by A1,FINSOP_1:7 .= a * (g "**" F) by VECTSP_1:def 10 .= a * Product F by Def3; end; theorem Th11: for G being unital (non empty HGrStr) holds Product <*> the carrier of G = 1.G proof let G be unital (non empty HGrStr); set g = the mult of G; A1: len <*> the carrier of G = 0 & g has_a_unity by FINSEQ_1:32,GROUP_1:34; thus Product <*> the carrier of G = g "**" (<*> the carrier of G) by Def3 .= the_unity_wrt g by A1,FINSOP_1:def 1 .= 1.G by GROUP_1:33; end; theorem Th12: for G being non empty HGrStr, a being Element of G holds Product<* a *> = a proof let G be non empty HGrStr, a be Element of G; thus Product<* a *> = (the mult of G) "**" <* a *> by Def3 .= a by FINSOP_1:12; end; theorem Th13: for G being non empty HGrStr, a,b being Element of G holds Product<* a,b *> = a * b proof let G be non empty HGrStr, a,b be Element of G; thus Product<* a,b *> = (the mult of G) "**" <* a,b *> by Def3 .= (the mult of G).(a,b) by FINSOP_1:13 .= a * b by VECTSP_1:def 10; end; theorem Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c) proof <* a,b,c *> = <* a *> ^ <* b,c *> & <* a,b,c *> = <* a,b *> ^ <* c *> & Product<* a *> = a & Product<* c *> = c & Product<* a,b *> = a * b & Product<* b,c *> = b * c by Th12,Th13,FINSEQ_1:60; hence thesis by Th8; end; Lm1: now let G,a; thus Product(0 |-> a) = Product <*> the carrier of G by FINSEQ_2:72 .= 1.G by Th11 .= a |^ 0 by GROUP_1:43; end; Lm2: now let G,a; let n; assume A1: Product(n |-> a) = a |^ n; thus Product((n + 1) |-> a) = Product((n |-> a) ^ <* a *>) by FINSEQ_2:74 .= Product(n |-> a) * Product<* a *> by Th8 .= a |^ n * a by A1,Th12 .= a |^ (n + 1) by GROUP_1:49; end; theorem Product(n |-> a) = a |^ n proof defpred P[Nat] means Product($1 |-> a) = a |^ $1; A1: P[0] by Lm1; A2: for n being Nat st P[n] holds P[n+1] by Lm2; for n being Nat holds P[n] from Ind(A1,A2); hence thesis; end; theorem Product(F - {1.G}) = Product(F) proof defpred P[FinSequence of the carrier of G] means Product($1 - {1.G}) = Product$1; A1: P[<*> the carrier of G] by FINSEQ_3:81; A2: for F,a st P[F] holds P[F ^ <* a *>] proof let F,a; assume A3: P[F]; A4: Product((F ^ <* a *>) - {1.G}) = Product(((F - {1.G}) ^ (<* a *> - {1.G}))) by FINSEQ_3:80 .= Product F * Product(<* a *> - {1.G}) by A3,Th8; now per cases; suppose A5: a = 1.G; then a in {1.G} by TARSKI:def 1; then <* a *> - {1.G} = <*> the carrier of G by FINSEQ_3:83; then Product(<* a *> - {1.G}) = 1.G by Th11; hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>) by A4,A5,Th9; suppose a <> 1.G; then not a in {1.G} by TARSKI:def 1; then <* a *> - {1.G} = <* a *> by FINSEQ_3:82; hence Product(F ^ <* a *> - {1.G}) = Product(F ^ <* a *>) by A4,Th8; end; hence thesis; end; for F holds P[F] from IndSeqD(A1,A2); hence thesis; end; Lm3: for F1 being FinSequence, y being Nat st y in dom F1 holds len F1 - y + 1 is Nat & len F1 - y + 1 >= 1 & len F1 - y + 1 <= len F1 proof let F1 be FinSequence, y be Nat; assume A1: y in dom F1; now assume len F1 - y + 1 < 0; then 1 < 0 - (len F1 - y) by REAL_1:86; then 1 < - (len F1 - y) by XCMPLX_1:150; then 1 < y - len F1 by XCMPLX_1:143; then len F1 + 1 < y & y <= len F1 by A1,FINSEQ_3:27,REAL_1:86; hence contradiction by NAT_1:37; end; then reconsider n = len F1 - y + 1 as Nat by INT_1:16; y + 0 <= len F1 by A1,FINSEQ_3:27; then A2: 0 + 1 = 1 & 0 <= len F1 - y by REAL_1:84; n - 1 <= len F1 - y & y >= 1 by A1,FINSEQ_3:27,REAL_1:86; then n - 1 - y <= len F1 - y - 1 by REAL_1:92; then n - (y + 1) <= len F1 - y - 1 by XCMPLX_1:36; then n - (y + 1) <= len F1 - (y + 1) by XCMPLX_1:36; hence thesis by A2,AXIOMS:24,REAL_1:54; end; theorem Th17: len F1 = len F2 & (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") implies Product(F1) = Product(F2)" proof defpred P[Nat] means for F1,F2 st len F1 = $1 & len F1 = len F2 & (for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)") holds Product(F1) = Product(F2)"; A1: P[0] proof let F1,F2; assume len F1 = 0 & len F1 = len F2; then F1 = <*> the carrier of G & F2 = <*> the carrier of G by FINSEQ_1:32; then Product F1 = 1.G & Product F2 = 1.G & 1.G = (1.G)" by Th11,GROUP_1:16; hence thesis; end; A2: for n st P[n] holds P[n + 1] proof let n; assume A3: P[n]; let F1,F2; assume that A4: len F1 = n + 1 & len F1 = len F2 and A5: for k st k in dom F1 holds F2.(len F1 - k + 1) = (F1/.k)"; reconsider p = F1 | Seg n as FinSequence of the carrier of G by FINSEQ_1:23; 1 <= n + 1 by NAT_1:37; then n + 1 in dom F1 by A4,FINSEQ_3:27; then F1.(n + 1) in rng F1 & rng F1 c= the carrier of G by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider a = F1.(n + 1) as Element of G; A6: len p = n by A4,FINSEQ_3:59; deffunc F(Nat) = F2.($1 + 1); consider q being FinSequence such that A7: len q = len p and A8: for k st k in Seg len p holds q.k = F(k) from SeqLambda; A9: dom q = dom p by A7,FINSEQ_3:31; A10: Seg len p = dom p by FINSEQ_1:def 3; rng q c= the carrier of G proof let x; assume x in rng q; then consider y such that A11: y in dom q & x = q.y by FUNCT_1:def 5; reconsider y as Nat by A11; A12: x = F2.(y + 1) by A8,A9,A10,A11; A13: 1 <= y + 1 by NAT_1:37; y <= len p by A7,A11,FINSEQ_3:27; then y + 1 <= len F2 by A4,A6,REAL_1:55; then y + 1 in dom F2 by A13,FINSEQ_3:27; then x in rng F2 & rng F2 c= the carrier of G by A12,FINSEQ_1:def 4,FUNCT_1:def 5; hence thesis; end; then reconsider q as FinSequence of the carrier of G by FINSEQ_1:def 4; A14: len F2 = len<* a" *> + len q by A4,A6,A7,FINSEQ_1:56; A15: now let k; assume k in dom<* a" *>; then A16: k in {1} by FINSEQ_1:4,def 8; len F2 >= 1 by A4,NAT_1:37; then A17: len F2 in dom F1 by A4,FINSEQ_3:27; then F2.(len F1 - len F1 + 1) = (F1/.len F1)" by A4,A5; then (F1/.len F1)" = F2.(0 + 1) by XCMPLX_1:14 .= F2.k by A16,TARSKI:def 1; then F2.k = a" & k = 1 by A4,A16,A17,FINSEQ_4:def 4,TARSKI:def 1; hence <* a" *>.k = F2.k by FINSEQ_1:def 8; end; now let k; assume k in dom q; then k in dom q & len<* a" *> = 1 & k + 1 = 1 + k by FINSEQ_1:56; hence F2.(len<* a" *> + k) = q.k by A8,A9,A10; end; then A18: F2 = <* a" *> ^ q by A14,A15,FINSEQ_3:43; now let k; assume A19: k in dom p; then reconsider i = len p - k + 1 as Nat by Lm3; 1 <= i & i <= len p by A19,Lm3; then i in dom p by FINSEQ_3:27; then A20: q.i = F2.(i + 1) by A8,A10; len p <= len F1 & k <= len p by A4,A6,A19,FINSEQ_3:27,NAT_1:37; then 1 <= k & k <= len F1 by A19,AXIOMS:22,FINSEQ_3:27; then A21: k in dom F1 by FINSEQ_3:27; A22: i + 1 = (len p + - k + 1) + 1 by XCMPLX_0:def 8 .= len F1 + - k + 1 by A4,A6,XCMPLX_1:1 .= len F1 - k + 1 by XCMPLX_0:def 8; F1/.k = F1.k by A21,FINSEQ_4:def 4 .= p.k by A19,FUNCT_1:70 .= p/.k by A19,FINSEQ_4:def 4; hence q.(len p - k + 1) = (p/.k)" by A5,A20,A21,A22; end; then A23: Product p = Product q" by A3,A6,A7; F1 = p ^ <* a *> by A4,FINSEQ_3:61; then A24: Product F1 = Product p * a by Th9; Product F2 = a" * Product q by A18,Th10 .= a" * Product p" by A23,GROUP_1:19 .= (Product p * a)" by GROUP_1:25; hence thesis by A24,GROUP_1:19; end; for k holds P[k] from Ind(A1,A2); hence thesis; end; theorem G is commutative Group implies for P being Permutation of dom F1 st F2 = F1 * P holds Product(F1) = Product(F2) proof set g = the mult of G; assume G is commutative Group; then A1: g is commutative & g has_a_unity & g is associative by GROUP_1:31,34,GROUP_3:2; let P be Permutation of dom F1; assume A2: F2 = F1 * P; thus Product(F1) = g "**" F1 by Def3 .= g "**" F2 by A1,A2,FINSOP_1:8 .= Product(F2) by Def3; end; theorem G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 implies Product(F1) = Product(F2) proof set g = the mult of G; assume G is commutative Group; then A1: g is commutative & g has_a_unity & g is associative by GROUP_1:31,34,GROUP_3:2; assume A2: F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2; thus Product(F1) = g "**" F1 by Def3 .= g "**" F2 by A1,A2,FINSOP_1:9 .= Product(F2) by Def3; end; theorem 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) proof set g = the mult of G; assume G is commutative Group; then A1: g is commutative & g has_a_unity & g is associative by GROUP_1:31,34,GROUP_3:2; assume A2: len F = len F1 & len F = len F2; assume A3: for k st k in dom F holds F.k = (F1/.k) * (F2/.k); A4: now let k; assume A5: k in dom F; A6: dom F = Seg len F & dom F1 = Seg len F1 & dom F2 = Seg len F2 by FINSEQ_1:def 3; thus F.k = (F1/.k) * (F2/.k) by A3,A5 .= g.(F1/.k,F2/.k) by VECTSP_1:def 10 .= g.(F1.k,F2/.k) by A2,A5,A6,FINSEQ_4:def 4 .= g.(F1.k,F2.k) by A2,A5,A6,FINSEQ_4:def 4; end; thus Product(F) = g "**" F by Def3 .= g.(g "**" F1,g "**" F2) by A1,A2,A4,FINSOP_1:10 .= (g "**" F1) * (g "**" F2) by VECTSP_1:def 10 .= Product(F1) * (g "**" F2) by Def3 .= Product(F1) * Product(F2) by Def3; end; theorem Th21: rng F c= carr H implies Product(F) in H proof defpred P[FinSequence of the carrier of G] means rng $1 c= carr H implies Product $1 in H; A1: P[<*> the carrier of G] proof assume rng <*> the carrier of G c= carr H; 1.G in H by GROUP_2:55; hence Product(<*> the carrier of G) in H by Th11; end; A2: now let F,d; assume A3: P[F]; thus P[F^<*d*>] proof assume A4: rng(F ^ <* d *>) c= carr H; rng F c= rng(F ^ <* d *>) & rng<* d *> c= rng(F ^ <* d *>) by FINSEQ_1:42,43; then rng F c= carr H & rng<* d *> c= carr H & rng<* d *> = {d} & d in {d} by A4,FINSEQ_1:56,TARSKI:def 1,XBOOLE_1:1; then d in H & Product(F) in H & Product(F ^ <* d *>) = Product(F) * d by A3,Th9,GROUP_2:88; hence Product(F ^ <* d *>) in H by GROUP_2:59; end; end; for F holds P[F] from IndSeqD(A1,A2); hence thesis; end; definition let G,I,F; func F |^ I -> FinSequence of the carrier of G means :Def4: len it = len F & for k st k in dom F holds it.k = (F/.k) |^ @(I/.k); existence proof deffunc F(Nat) = (F/.$1) |^ @(I/.$1); consider p being FinSequence such that A1: len p = len F and A2: for k st k in Seg len F holds p.k = F(k) from SeqLambda; A3: dom p = dom F by A1,FINSEQ_3:31; A4: dom F = Seg len F by FINSEQ_1:def 3; rng p c= the carrier of G proof let x; assume x in rng p; then consider y such that A5: y in dom p & p.y = x by FUNCT_1:def 5; reconsider y as Nat by A5; x = (F/.y) |^ @(I/.y) & (F/.y) |^ @(I/.y) in the carrier of G by A2,A3,A4,A5; hence thesis; end; then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4; take p; thus thesis by A1,A2,A4; end; uniqueness proof let F1,F2; assume that A6: len F1 = len F and A7: for k st k in dom F holds F1.k = (F/.k) |^ @(I/.k); assume that A8: len F2 = len F and A9: for k st k in dom F holds F2.k = (F/.k) |^ @(I/.k); now let k; assume k in Seg len F; then A10: k in dom F by FINSEQ_1:def 3; hence F1.k = (F/.k) |^ @(I/.k) by A7 .= F2.k by A9,A10; end; hence thesis by A6,A8,FINSEQ_2:10; end; end; canceled 3; theorem Th25: len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2) = (F1 |^ I1) ^ (F2 |^ I2) proof assume A1: len F1 = len I1 & len F2 = len I2; set q = F1 |^ I1; set r = F2 |^ I2; A2: len(q ^ r) = len q + len r by FINSEQ_1:35 .= len F1 + len r by Def4 .= len F1 + len F2 by Def4 .= len(F1 ^ F2) by FINSEQ_1:35; len(F1 ^ F2) = len F1 + len F2 by FINSEQ_1:35 .= len(I1 ^ I2) by A1,FINSEQ_1:35; then A3: dom (F1 ^ F2) = dom (I1 ^ I2) by FINSEQ_3:31; now let k; assume A4: k in dom(F1 ^ F2); now per cases by A4,FINSEQ_1:38; suppose A5: k in dom F1; then A6: k in dom I1 by A1,FINSEQ_3:31; then A7: I1/.k = I1.k by FINSEQ_4:def 4; A8: (I1 ^ I2).k = (I1 ^ I2)/.k by A3,A4,FINSEQ_4:def 4; len q = len F1 by Def4; then k in dom q by A5,FINSEQ_3:31; then A9: (q ^ r).k = q.k by FINSEQ_1:def 7 .= (F1/.k) |^ @(I1/.k) by A5,Def4; F1/.k = F1.k by A5,FINSEQ_4:def 4 .= (F1 ^ F2).k by A5,FINSEQ_1:def 7 .= (F1 ^ F2)/.k by A4,FINSEQ_4:def 4; hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A6,A7,A8,A9,FINSEQ_1:def 7; suppose ex n st n in dom F2 & k = len F1 + n; then consider n such that A10: n in dom F2 and A11: k = len F1 + n; A12: len r = len F2 & len q = len F1 by Def4; then A13: n in dom r & n in dom I2 by A1,A10,FINSEQ_3:31; then A14: (q ^ r).k = r.n & (I1 ^ I2).k = I2.n & (F1 ^ F2).k = F2.n & n in dom F2 & (F1 ^ F2).k = (F1 ^ F2)/.k & F2.n = F2/.n by A1,A4,A10,A11,A12,FINSEQ_1:def 7,FINSEQ_4:def 4; A15: (I1 ^ I2)/.k = (I1 ^ I2).k by A3,A4,FINSEQ_4:def 4; I2/.n = I2.n by A13,FINSEQ_4:def 4; hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k) by A14,A15,Def4 ; end; hence (q ^ r).k = ((F1 ^ F2)/.k) |^ @((I1 ^ I2)/.k); end; hence thesis by A2,Def4; end; theorem Th26: rng F c= carr H implies Product(F |^ I) in H proof assume that A1: rng F c= carr H; rng(F |^ I) c= carr H proof let x; assume x in rng(F |^ I); then consider y such that A2: y in dom(F |^ I) & x = (F |^ I).y by FUNCT_1:def 5; reconsider y as Nat by A2; len(F |^ I) = len F by Def4; then A3: y in dom F by A2,FINSEQ_3:31; then A4: x = (F/.y) |^ @(I/.y) by A2,Def4; F.y in rng F & F.y = F/.y by A3,FINSEQ_4:def 4,FUNCT_1:def 5; then F/.y in H by A1,GROUP_2:88; then x in H by A4,Th6; hence thesis by GROUP_2:88; end; hence thesis by Th21; end; theorem Th27: (<*> the carrier of G) |^ (<*> INT) = {} proof len <*> the carrier of G = 0 & len <*> INT = 0 by FINSEQ_1:32; then len((<*> the carrier of G) |^ (<*> INT)) = 0 by Def4; hence thesis by FINSEQ_1:25; end; theorem Th28: <* a *> |^ <* @i *> = <* a |^ i *> proof A1: len<* a *> = 1 & len<* @i *> = 1 & len<* a |^ i*> = 1 by FINSEQ_1:56; now let k; assume A2: k in dom <* a *>; A3: i = @i & @i = <* @i *>/.1 by Def2,FINSEQ_4:25; dom <* a *> = Seg len <* a *> by FINSEQ_1:def 3; then A4: k = 1 by A1,A2,FINSEQ_1:4,TARSKI:def 1; hence <* a |^ i *>.k = a |^ i by FINSEQ_1:57 .= (<* a *>/.k) |^ @(<* @i *>/.k) by A3,A4,FINSEQ_4:25; end; hence thesis by A1,Def4; end; theorem Th29: <* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *> proof len<* a *> = 1 & len<* b *> = 1 & len <* @i *> = 1 & len<* @j *> = 1 & <* a,b *> = <* a *> ^ <* b *> & <* @i,@j *> = <* @i *> ^ <* @j *> by FINSEQ_1:56,def 9; hence <* a,b *> |^ <* @i,@j *> = (<* a *> |^ <* @i *>) ^ (<* b *> |^ <* @j *>) by Th25 .= <* a |^ i *> ^ (<* b *> |^ <* @j *>) by Th28 .= <* a |^ i *> ^ <* b |^ j *> by Th28 .= <* a |^ i,b |^ j *> by FINSEQ_1:def 9; end; theorem <* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *> proof len<* a *> = 1 & len<* b,c *> = 2 & len <* @i1 *> = 1 & len<* @i2,@i3 *> = 2 & <* a,b,c *> = <* a *> ^ <* b,c *> & <* @i1,@i2,@i3 *> = <* @i1 *> ^ <* @i2,@i3 *> by FINSEQ_1:56,60,61; hence <* a,b,c *> |^ <* @i1,@i2,@i3 *> = (<* a *> |^ <* @i1 *>) ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th25 .= <* a |^ i1 *> ^ (<* b,c *> |^ <* @i2,@i3 *>) by Th28 .= <* a |^ i1 *> ^ <* b |^ i2,c |^ i3 *> by Th29 .= <* a |^ i1,b |^ i2,c |^ i3 *> by FINSEQ_1:60; end; theorem F |^ (len F |-> @(1)) = F proof defpred P[FinSequence of the carrier of G] means $1 |^ (len $1 |-> @(1)) = $1; A1: P[<*> the carrier of G] proof set A = <*> the carrier of G; thus A |^ (len A |-> @(1)) = A |^ (0 |-> @(1)) by FINSEQ_1:32 .= A |^ (<*> INT) by FINSEQ_2:72 .= A by Th27; end; A2: for F,a st P[F] holds P[F ^ <* a *>] proof let F,a; set A = F ^ <* a *>; assume A3: P[F]; A4: len A = len F + len<* a *> by FINSEQ_1:35; A5: len<* a *> = 1 by FINSEQ_1:57; A6: len<* @(1) *> = 1 by FINSEQ_1:57; A7: len(len F |-> @(1)) = len F by FINSEQ_2:69; thus A |^ (len A |-> @(1)) = A |^ ((len F |-> @(1)) ^ <* @(1) *>) by A4,A5,FINSEQ_2:74 .= (F |^ (len F |-> @(1))) ^ (<* a *> |^ <* @(1) *>) by A5,A6,A7,Th25 .= F ^ <* a |^ 1 *> by A3,Th28 .= F ^ <* a *> by GROUP_1:44; end; for F holds P[F] from IndSeqD(A1,A2); hence thesis; end; theorem F |^ (len F |-> @(0)) = len F |-> 1.G proof defpred P[FinSequence of the carrier of G] means $1 |^ (len $1 |-> @(0)) = len $1 |-> 1.G; A1: P[<*> the carrier of G] proof set A = <*> the carrier of G; A2: len A = 0 by FINSEQ_1:32; thus A |^ (len A |-> @(0)) = A |^ (0 |-> @(0)) by FINSEQ_1:32 .= A |^ (<*> INT) by FINSEQ_2:72 .= {} by Th27 .= len A |-> 1.G by A2,FINSEQ_2:72; end; A3: for F,a st P[F] holds P[F ^ <* a *>] proof let F,a; set A = F ^ <* a *>; assume A4: P[F]; A5: len A = len F + len<* a *> by FINSEQ_1:35; A6: len<* a *> = 1 by FINSEQ_1:57; A7: len<* @(0) *> = 1 by FINSEQ_1:57; A8: len(len F |-> @(0)) = len F by FINSEQ_2:69; thus A |^ (len A |-> @(0)) = A |^ ((len F |-> @(0)) ^ <* @(0) *>) by A5,A6,FINSEQ_2:74 .= (F |^ (len F |-> @(0))) ^ (<* a *> |^ <* @(0) *>) by A6,A7,A8,Th25 .= (len F |-> 1.G) ^ <* a |^ 0 *> by A4,Th28 .= (len F |-> 1.G) ^ <* 1.G *> by GROUP_1:43 .= (len A |-> 1.G) by A5,A6,FINSEQ_2:74; end; for F holds P[F] from IndSeqD(A1,A3); hence thesis; end; theorem len I = n implies (n |-> 1.G) |^ I = n |-> 1.G proof defpred P[Nat] means for I st len I = $1 holds ($1 |-> 1.G) |^ I = $1 |-> 1.G; A1: P[0] proof let I; assume len I = 0; then I = <*> INT & (0 |-> 1.G) = {} & {} = <*> the carrier of G by FINSEQ_1:32,FINSEQ_2:72; hence (0 |-> 1.G) |^ I = 0 |-> 1.G by Th27; end; A2: for k st P[k] holds P[k + 1] proof let k; assume A3: P[k]; let I; assume A4: len I = k + 1; reconsider J = I | Seg k as FinSequence of INT by FINSEQ_1:23; A5: len J = k by A4,FINSEQ_3:59; then A6: (k |-> 1.G) |^ J = k |-> 1.G by A3; 1 <= k + 1 by NAT_1:37; then k + 1 in dom I by A4,FINSEQ_3:27; then I.(k + 1) in rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider i = I.(k + 1) as Integer by INT_1:12; A7: I = J ^ <* i *> by A4,FINSEQ_3:61 .= J ^ <* @i *> by Def2; A8: (k + 1) |-> 1.G = (k |-> 1.G) ^ <* 1.G *> by FINSEQ_2:74; len(k |-> 1.G) = k & len<* 1.G *> = 1 & len<* @i *> = 1 by FINSEQ_1:57,FINSEQ_2:69; then ((k + 1) |-> 1.G) |^ I = ((k |-> 1.G) |^ J) ^ (<* 1.G *> |^ <* @i *>) by A5,A7,A8,Th25 .= (k |-> 1.G) ^ <* (1.G) |^ i *> by A6,Th28 .= (k |-> 1.G) ^ <* 1.G *> by GROUP_1:61; hence thesis by FINSEQ_2:74; end; for k holds P[k] from Ind(A1,A2); hence thesis; end; definition let G,A; func gr A -> strict Subgroup of G means :Def5: 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 proof defpred P[set] means ex H st $1 = carr H & A c= $1; consider X such that A1: Y in X iff Y in bool the carrier of G & P[Y] from Separation; set M = meet X; A2: the carrier of G in bool the carrier of G & the carrier of the HGrStr of G = the carrier of (Omega).G & A c= the carrier of G & carr (Omega).G = the carrier of (Omega). G by GROUP_2:def 8,def 9,ZFMISC_1:def 1; then A3: the carrier of G in X by A1; A4: X <> {} by A1,A2; now let Y; assume Y in X; then consider H such that A5: Y = carr H and A c= Y by A1; 1.G in H by GROUP_2:55; hence 1.G in Y by A5,GROUP_2:88; end; then A6: M <> {} by A4,SETFAM_1:def 1; M c= the carrier of G proof consider x such that A7: x in X by A3; consider H such that A8: x = carr H and A c= x by A1,A7; let y; assume y in M; then y in carr H & carr H c= the carrier of G by A7,A8,SETFAM_1:def 1; hence thesis; end; then reconsider M as Subset of G; A9: now let a,b; assume A10: a in M & b in M; now let Y; assume A11: Y in X; then consider H such that A12: Y = carr H and A c= Y by A1; a in carr H & b in carr H by A10,A11,A12,SETFAM_1:def 1; hence a * b in Y by A12,GROUP_2:89; end; hence a * b in M by A4,SETFAM_1:def 1; end; now let a; assume A13: a in M; now let Y; assume A14: Y in X; then consider H such that A15: Y = carr H and A c= Y by A1; a in carr H by A13,A14,A15,SETFAM_1:def 1; hence a" in Y by A15,GROUP_2:90; end; hence a" in M by A4,SETFAM_1:def 1; end; then consider H being strict Subgroup of G such that A16: the carrier of H = M by A6,A9,GROUP_2:61; take H; now let Y; assume Y in X; then ex H st Y = carr H & A c= Y by A1; hence A c= Y; end; hence A c= the carrier of H by A4,A16,SETFAM_1:6; let H1 be strict Subgroup of G; assume A17: A c= the carrier of H1; the carrier of H1 = carr H1 by GROUP_2:def 9; then the carrier of H1 in X by A1,A17; then M c= the carrier of H1 by SETFAM_1:4; hence H is Subgroup of H1 by A16,GROUP_2:66; end; uniqueness proof let H1,H2 be strict Subgroup of G; assume A c= the carrier of H1 & (for H being strict Subgroup of G st A c= the carrier of H holds H1 is Subgroup of H) & A c= the carrier of H2 & (for H being strict Subgroup of G st A c= the carrier of H holds H2 is Subgroup of H); then H1 is Subgroup of H2 & H2 is Subgroup of H1; hence thesis by GROUP_2:64; end; end; canceled 3; theorem Th37: a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a proof thus a in gr A implies ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a proof assume A1: a in gr A; defpred P[set] means ex F,I st $1 = Product (F |^ I) & len F = len I & rng F c= A; reconsider B = {b : P[b]} as Subset of G from SubsetD; 1.G = Product <*> the carrier of G & <*> the carrier of G = {} & (<*> the carrier of G) |^ (<*> INT) = {} & rng <*> the carrier of G = {} & {} c= A & len {} = 0 & len<*>INT = 0 by Th11,Th27,FINSEQ_1:25,27,XBOOLE_1:2; then A2: 1.G in B; A3: now let c,d; assume that A4: c in B and A5: d in B; A6: ex d1 being Element of G st c = d1 & ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A by A4; A7: ex d2 being Element of G st d = d2 & ex F,I st d2 = Product(F |^ I) & len F = len I & rng F c= A by A5; consider F1,I1 such that A8: c = Product(F1 |^ I1) and A9: len F1 = len I1 and A10: rng F1 c= A by A6; consider F2,I2 such that A11: d = Product(F2 |^ I2) and A12: len F2 = len I2 and A13: rng F2 c= A by A7; A14: c * d = Product((F1 |^ I1) ^ (F2 |^ I2)) by A8,A11,Th8 .= Product((F1 ^ F2) |^ (I1 ^ I2)) by A9,A12,Th25; rng(F1 ^ F2) = rng F1 \/ rng F2 by FINSEQ_1:44; then A15: rng(F1 ^ F2) c= A by A10,A13,XBOOLE_1:8; len(F1 ^ F2) = len I1 + len I2 by A9,A12,FINSEQ_1:35 .= len(I1 ^ I2) by FINSEQ_1:35; hence c * d in B by A14,A15; end; now let c; assume c in B; then ex d1 being Element of G st c = d1 & ex F,I st d1 = Product(F |^ I) & len F = len I & rng F c= A; then consider F1,I1 such that A16: c = Product(F1 |^ I1) and A17: len F1 = len I1 and A18: rng F1 c= A; A19: dom F1 = dom I1 by A17,FINSEQ_3:31; deffunc F(Nat) = F1.(len F1 - $1 + 1); consider F2 being FinSequence such that A20: len F2 = len F1 and A21: for k st k in Seg len F1 holds F2.k = F(k) from SeqLambda; A22: dom F2 = dom F1 by A20,FINSEQ_3:31; A23: Seg len F1 = dom F1 by FINSEQ_1:def 3; defpred P[Nat,set] means ex i st i = I1.(len I1 - $1 + 1) & $2 = - i; A24: for k,y1,y2 st k in Seg len I1 & P[k,y1] & P[k,y2] holds y1 = y2; A25: for k st k in Seg len I1 ex x st P[k,x] proof let k; assume k in Seg len I1; then A26: k in dom I1 by FINSEQ_1:def 3; then reconsider n = len I1 - k + 1 as Nat by Lm3; 1 <= n & n <= len I1 by A26,Lm3; then n in dom I1 by FINSEQ_3:27; then I1.n in rng I1 & rng I1 c= INT by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider i = I1.n as Element of INT qua non empty set; reconsider i as Integer; reconsider x = - i as set; take x,i; thus thesis; end; consider I2 being FinSequence such that A27: dom I2 = Seg len I1 and A28: for k st k in Seg len I1 holds P[k,I2.k] from SeqEx(A24,A25); A29: Seg len I1 = dom I1 by FINSEQ_1:def 3; A30: len F2 = len I2 by A17,A20,A27,FINSEQ_1:def 3; A31: dom F2 = dom I2 by A17,A20,A27,FINSEQ_1:def 3; A32: rng F2 c= rng F1 proof let x; assume x in rng F2; then consider y such that A33: y in dom F2 & F2.y = x by FUNCT_1:def 5; reconsider y as Nat by A33; A34: x = F1.(len F1 - y + 1) by A21,A22,A23,A33; reconsider n = len F1 - y + 1 as Nat by A20,A33,Lm3; A35: 1 <= n by A20,A33,Lm3; n <= len F1 by A20,A33,Lm3; then n in dom F1 by A35,FINSEQ_3:27; hence thesis by A34,FUNCT_1:def 5; end; then A36: rng F2 c= A by A18,XBOOLE_1:1; rng F1 c= the carrier of G by FINSEQ_1:def 4; then rng F2 c= the carrier of G by A32,XBOOLE_1:1; then reconsider F2 as FinSequence of the carrier of G by FINSEQ_1:def 4; rng I2 c= INT proof let x; assume x in rng I2; then consider y such that A37: y in dom I2 and A38: x = I2.y by FUNCT_1:def 5; reconsider y as Nat by A37; ex i st i = I1.(len I1 - y + 1) & x = - i by A27,A28,A37,A38; hence thesis by INT_1:12; end; then reconsider I2 as FinSequence of INT by FINSEQ_1:def 4; set p = F1 |^ I1; set q = F2 |^ I2; A39: len p = len F1 & len q = len F2 by Def4; then A40: dom p = dom F1 & dom q = dom F2 by FINSEQ_3:31; now let k; assume A41: k in dom q; then reconsider n = len p - k + 1 as Nat by A20,A39,Lm3; 1 <= n & len p >= n by A20,A39,A41,Lm3; then A42: n in dom I2 & n in Seg len I2 by A20,A30,A39,FINSEQ_1:3,FINSEQ_3:27; dom q = dom I1 by A17,A20,A39,FINSEQ_3:31; then consider i such that A43: i = I1.n & I2.k = - i by A17,A28, A29,A39,A41; I2.k = I2/.k & I2/.k = @(I2/.k) by A31,A40,A41,Def2,FINSEQ_4:def 4; then q.k = (F2/.k) |^ (- i) & F2/.k = F2.k & F2.k = F1.n & F1/.n= F1.n by A17,A21,A22,A23,A27,A39,A40,A41,A42,A43,Def4, FINSEQ_4:def 4; then A44: q.k = ((F1/.n) |^ i)" by GROUP_1:70; I1.n = I1/.n & I1/.n = @(I1/.n) by A27,A29,A42,Def2,FINSEQ_4:def 4; then p.n = (F1/.n) |^ i by A19,A27,A29,A42,A43,Def4; then (p/.n)" = ((F1/.n) |^ i)" & q/.k = q.k by A19,A27,A29,A40,A41,A42,FINSEQ_4:def 4; then p/.n = (q/.k)" by A44,GROUP_1:19; hence (q/.k)" = p.(len p - k + 1) by A19,A27,A29,A40,A42,FINSEQ_4:def 4; end; then Product p" = Product q by A20,A39,Th17; hence c" in B by A16,A30,A36; end; then consider H being strict Subgroup of G such that A45: the carrier of H = B by A2,A3,GROUP_2:61; A c= B proof let x; assume A46: x in A; then reconsider a = x as Element of G; reconsider p = 1 as Integer; A47: len<* a *> = 1 & len<* @p *> = 1 by FINSEQ_1:56; A48: Product(<* a *> |^ <* @p *>) = Product<* a |^ 1 *> by Th28 .= a |^ 1 by Th12 .= a by GROUP_1:44; rng<* a *> = {a} & {a} c= A by A46,FINSEQ_1:56,ZFMISC_1:37; hence thesis by A47,A48; end; then gr A is Subgroup of H by A45,Def5; then a in H by A1,GROUP_2:49; then a in B by A45,RLVECT_1:def 1; then ex b st b = a & ex F,I st b = Product(F |^ I) & len F = len I & rng F c= A; hence thesis; end; given F,I such that len F = len I and A49: rng F c= A and A50: Product(F |^ I) = a; A c= the carrier of gr A by Def5; then A c= carr gr A by GROUP_2:def 9; then rng F c= carr gr A by A49,XBOOLE_1:1; hence thesis by A50,Th26; end; theorem Th38: a in A implies a in gr A proof assume A1: a in A; A c= the carrier of gr A by Def5; hence thesis by A1,RLVECT_1:def 1; end; theorem gr {} the carrier of G = (1).G proof A1: {} the carrier of G c= the carrier of (1).G by XBOOLE_1:2; for H being strict Subgroup of G st {} the carrier of G c= the carrier of H holds (1).G is Subgroup of H by GROUP_2:77; hence thesis by A1,Def5; end; theorem Th40: for H being strict Subgroup of G holds gr carr H = H proof let H be strict Subgroup of G; A1: carr H = the carrier of H by GROUP_2:def 9; now let H1 be strict Subgroup of G; assume carr H c= the carrier of H1; then the carrier of H c= the carrier of H1 by GROUP_2:def 9; hence H is Subgroup of H1 by GROUP_2:66; end; hence thesis by A1,Def5; end; theorem Th41: A c= B implies gr A is Subgroup of gr B proof assume A1: A c= B; now let a; assume a in gr A; then consider F,I such that A2: len F = len I & rng F c= A & Product(F |^ I) = a by Th37; rng F c= B by A1,A2,XBOOLE_1:1; hence a in gr B by A2,Th37; end; hence thesis by GROUP_2:67; end; theorem gr(A /\ B) is Subgroup of gr A /\ gr B proof now let a; assume a in gr(A /\ B); then consider F,I such that A1: len F = len I & rng F c= A /\ B & Product(F |^ I) = a by Th37; A /\ B c= A & A /\ B c= B by XBOOLE_1:17; then rng F c= A & rng F c= B by A1,XBOOLE_1:1; then a in gr A & a in gr B by A1,Th37; hence a in gr A /\ gr B by GROUP_2:99; end; hence thesis by GROUP_2:67; end; theorem Th43: the carrier of gr A = meet{B : ex H being strict Subgroup of G st B = the carrier of H & A c= carr H} proof defpred P[Subgroup of G] means A c= carr $1; A1: A c= the carrier of G & the carrier of (Omega).G = carr (Omega).G & (Omega).G = the HGrStr of G by GROUP_2:def 8,def 9; then A2: ex H being strict Subgroup of G st P[H]; consider H being strict Subgroup of G such that A3: the carrier of H = meet{B : ex H being strict Subgroup of G st B = the carrier of H & P[H]} from MeetSbgEx(A2); set X = {B :ex H being strict Subgroup of G st B = the carrier of H & A c= carr H}; A4: carr (Omega).G in X by A1; now let Y; assume Y in X; then ex B st Y = B & ex H being strict Subgroup of G st B = the carrier of H & A c= carr H; hence A c= Y by GROUP_2:def 9; end; then A5: A c= the carrier of H by A3,A4,SETFAM_1:6; now let H1 be strict Subgroup of G; assume A6: A c= the carrier of H1; the carrier of H1 = carr H1 by GROUP_2:def 9; then the carrier of H1 in X by A6; then the carrier of H c= the carrier of H1 by A3,SETFAM_1:4; hence H is Subgroup of H1 by GROUP_2:66; end; hence thesis by A3,A5,Def5; end; theorem Th44: gr A = gr(A \ {1.G}) proof set X = {B : ex H being strict Subgroup of G st B = the carrier of H & A c= carr H}; set Y = {C : ex H being strict Subgroup of G st C = the carrier of H & A \ {1.G} c= carr H}; A1: X = Y proof thus X c= Y proof let x; assume x in X; then consider B such that A2: x = B and A3: ex H being strict Subgroup of G st B = the carrier of H & A c= carr H; consider H being strict Subgroup of G such that A4: B = the carrier of H and A5: A c= carr H by A3 ; A \ {1.G} c= A by XBOOLE_1:36; then A \ {1.G} c= carr H by A5,XBOOLE_1:1; hence thesis by A2,A4; end; let x; assume x in Y; then consider B such that A6: x = B and A7: ex H being strict Subgroup of G st B = the carrier of H & A \ {1.G} c= carr H; consider H being strict Subgroup of G such that A8: B = the carrier of H and A9: A \ {1.G} c= carr H by A7; 1.G in H by GROUP_2:55; then 1.G in carr H by GROUP_2:88; then {1.G} c= carr H by ZFMISC_1:37; then A10: (A \ {1.G}) \/ {1.G} c= carr H by A9,XBOOLE_1:8; now per cases; suppose 1.G in A; then {1.G} c= A by ZFMISC_1:37; hence A c= carr H by A10,XBOOLE_1:45; suppose not 1.G in A; hence A c= carr H by A9,ZFMISC_1:65; end; hence thesis by A6,A8; end; the carrier of gr A = meet X by Th43 .= the carrier of gr(A \ {1.G}) by A1,Th43; hence thesis by GROUP_2:68; end; definition let G,a; attr a is generating means :Def6: not for A st gr A = the HGrStr of G holds gr(A \ {a}) = the HGrStr of G; end; canceled; theorem 1.G is non generating proof let A; assume gr A = the HGrStr of G; hence thesis by Th44; end; definition let G, H; attr H is maximal means :Def7: 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 Th48: 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 proof let G be strict Group, H be strict Subgroup of G, a be Element of G; assume that A1: H is maximal and A2: not a in H; a in {a} by TARSKI:def 1; then carr H c= carr H \/ {a} & a in carr H \/ {a} by XBOOLE_0:def 2,XBOOLE_1:7; then gr carr H is Subgroup of gr(carr H \/ {a}) & a in gr(carr H \/ {a}) by Th38,Th41; then H is Subgroup of gr(carr H \/ {a}) & H <> gr(carr H \/ {a}) by A2,Th40; hence thesis by A1,Def7; end; :: :: Frattini subgroup. :: definition let G be Group; func Phi(G) -> strict Subgroup of G means :Def8: 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; existence proof defpred P[Subgroup of G] means $1 is maximal; now per cases; suppose A1: ex H being strict Subgroup of G st P[H]; 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]} from MeetSbgEx(A1); hence thesis by A1; suppose A2: for H being strict Subgroup of G holds H is not maximal; (Omega).G = the HGrStr of G & (Omega).G is Subgroup of G by GROUP_2:def 8; hence thesis by A2; end; hence thesis; end; uniqueness by GROUP_2:68; correctness; end; canceled 3; theorem Th52: 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) proof let G be Group; assume A1: ex H being strict Subgroup of G st H is maximal; set X = {A where A is Subset of G: ex K being strict Subgroup of G st A = the carrier of K & K is maximal}; thus a in Phi(G) implies for H being strict Subgroup of G st H is maximal holds a in H proof assume a in Phi(G); then a in the carrier of Phi(G) by RLVECT_1:def 1; then A2: a in meet X by A1,Def8; let H be strict Subgroup of G; assume A3: H is maximal; the carrier of H = carr H by GROUP_2:def 9; then carr H in X by A3; then a in carr H by A2,SETFAM_1:def 1; hence thesis by GROUP_2:88; end; consider H being strict Subgroup of G such that A4: H is maximal by A1; carr H = the carrier of H by GROUP_2:def 9; then A5: carr H in X by A4; assume A6: for H being strict Subgroup of G st H is maximal holds a in H; now let Y; assume Y in X; then consider A being Subset of G such that A7: Y = A and A8: ex H being strict Subgroup of G st A = the carrier of H & H is maximal; consider H being strict Subgroup of G such that A9: A = the carrier of H & H is maximal by A8; A = carr H & a in H by A6,A9,GROUP_2:def 9; hence a in Y by A7,GROUP_2:88; end; then a in meet X by A5,SETFAM_1:def 1; then a in the carrier of Phi(G) by A1,Def8; hence thesis by RLVECT_1:def 1; end; theorem 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) proof let G be Group, a be Element of G; assume for H being strict Subgroup of G holds H is not maximal; then Phi(G) = the HGrStr of G by Def8; hence thesis by RLVECT_1:def 1; end; theorem Th54: for G being Group, H being strict Subgroup of G holds H is maximal implies Phi(G) is Subgroup of H proof let G be Group, H be strict Subgroup of G; assume H is maximal; then for a be Element of G holds a in Phi(G) implies a in H by Th52; hence thesis by GROUP_2:67; end; theorem Th55: for G being strict Group holds the carrier of Phi(G) = {a where a is Element of G: a is non generating} proof let G be strict Group; set A = {a where a is Element of G: a is non generating}; thus the carrier of Phi(G) c= A proof let x; assume A1: x in the carrier of Phi(G); assume A2: not x in A; x in Phi(G) by A1,RLVECT_1:def 1; then x in G by GROUP_2:49; then reconsider a = x as Element of G by RLVECT_1:def 1; a is generating by A2; then consider B being Subset of G such that A3: gr B = G and A4: gr(B \ {a}) <> G by Def6; set M = B \ {a}; defpred P[Subgroup of G] means M c= carr $1 & not a in $1; consider X such that A5: X c= Subgroups G and A6: for H being strict Subgroup of G holds H in X iff P[H] from SubgrSep; M c= the carrier of gr M by Def5; then A7: M c= carr gr M by GROUP_2:def 9; now assume A8: a in gr M; now let b be Element of G; b in gr B by A3,RLVECT_1:def 1; then consider F being FinSequence of the carrier of G, I such that len I = len F and A9: rng F c= B and A10: b = Product(F |^ I) by Th37; rng(F |^ I) c= carr gr M proof let x; assume x in rng(F |^ I); then consider y such that A11: y in dom(F |^ I) and A12: (F |^ I).y = x by FUNCT_1:def 5; reconsider y as Nat by A11; len(F |^ I) = len F by Def4; then A13: y in dom F by A11,FINSEQ_3:31; then A14: x = (F/.y) |^ @(I/.y) by A12,Def4; now per cases; suppose F/.y = a; then x in gr M by A8,A14,Th6; hence thesis by GROUP_2:88; suppose A15: F/.y <> a; F/.y = F.y & F.y in rng F by A13,FINSEQ_4:def 4,FUNCT_1:def 5; then F/.y in B & not F/.y in {a} by A9,A15,TARSKI:def 1; then F/.y in M by XBOOLE_0:def 4; then F/.y in gr M by Th38; then x in gr M by A14,Th6; hence thesis by GROUP_2:88; end; hence thesis; end; hence b in gr M by A10,Th21; end; hence contradiction by A4,GROUP_2:71; end; then reconsider X as non empty set by A6,A7; defpred P[set,set] means ex H1,H2 being strict Subgroup of G st $1 = H1 & $2 = H2 & H1 is Subgroup of H2; A16: now let x be Element of X; x in Subgroups G by A5,TARSKI:def 3; hence x is strict Subgroup of G by GROUP_3:def 1; end; A17: for x being Element of X holds P[x,x] proof let x be Element of X; reconsider H = x as strict Subgroup of G by A16; H is Subgroup of H by GROUP_2:63; hence thesis; end; A18: for x,y being Element of X st P[x,y] & P[y,x] holds x = y by GROUP_2:64; A19: for x,y,z being Element of X st P[x,y] & P[y,z] holds P[x,z] proof let x,y,z be Element of X; given H1,H2 being strict Subgroup of G such that A20: x = H1 & y = H2 & H1 is Subgroup of H2; given H3,H4 being strict Subgroup of G such that A21: y = H3 & z = H4 & H3 is Subgroup of H4; H1 is Subgroup of H4 by A20,A21,GROUP_2:65; hence thesis by A20,A21; end; A22: for Y st Y c= X & (for x,y being Element of X st x in Y & y in Y holds P[x,y] or P[y,x]) ex y being Element of X st for x being Element of X st x in Y holds P[x,y] proof let Y; assume A23: Y c= X; assume A24: for x,y being Element of X st x in Y & y in Y holds P[x,y] or P[y,x]; set C = {D where D is Subset of G : ex H being strict Subgroup of G st H in Y & D = carr H}; now let Z be set; assume Z in C; then ex D being Subset of G st Z = D & ex H being strict Subgroup of G st H in Y & D = carr H; hence Z c= the carrier of G; end; then reconsider E = union C as Subset of G by ZFMISC_1:94; now per cases; suppose A25: Y = {}; consider y being Element of X; take y; let x be Element of X; assume x in Y; hence P[x,y] by A25; suppose A26: Y <> {}; consider s being Element of Y; A27: s in X by A23,A26,TARSKI:def 3; then reconsider s as strict Subgroup of G by A5,GROUP_3:def 1; A28: carr s in C by A26; then carr s c= E & M c= carr s by A6,A27,ZFMISC_1:92; then A29: M c= E by XBOOLE_1:1; carr s <> {} by GROUP_2:87; then A30: E <> {} by A28,ORDERS_1:91; A31: now let a,b be Element of G; assume that A32: a in E and A33: b in E; consider Z being set such that A34: a in Z and A35: Z in C by A32,TARSKI: def 4; consider D being Subset of G such that A36: Z = D and A37: ex H being strict Subgroup of G st H in Y & D = carr H by A35; consider H1 being Subgroup of G such that A38: H1 in Y & D = carr H1 by A37; consider Z1 being set such that A39: b in Z1 and A40: Z1 in C by A33,TARSKI:def 4; consider B being Subset of G such that A41: Z1 = B and A42: ex H being strict Subgroup of G st H in Y & B = carr H by A40; consider H2 being Subgroup of G such that A43: H2 in Y & B = carr H2 by A42; now per cases by A23,A24,A38,A43; suppose P[H1,H2]; then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5; then carr H1 c= the carrier of H2 by GROUP_2:def 9; then carr H1 c= carr H2 by GROUP_2:def 9; then a * b in carr H2 by A34,A36,A38,A39,A41,A43, GROUP_2:89; hence a * b in E by A40,A41,A43,TARSKI:def 4; suppose P[H2,H1]; then the carrier of H2 c= the carrier of H1 by GROUP_2:def 5; then carr H2 c= the carrier of H1 by GROUP_2:def 9; then carr H2 c= carr H1 by GROUP_2:def 9; then a * b in carr H1 by A34,A36,A38,A39,A41,A43, GROUP_2:89; hence a * b in E by A35,A36,A38,TARSKI:def 4; end; hence a * b in E; end; now let a be Element of G; assume a in E; then consider Z being set such that A44: a in Z and A45: Z in C by TARSKI:def 4; consider D being Subset of G such that A46: Z = D and A47: ex H being strict Subgroup of G st H in Y & D = carr H by A45; consider H1 being Subgroup of G such that A48: H1 in Y & D = carr H1 by A47; a" in carr H1 by A44,A46,A48,GROUP_2:90; hence a" in E by A45,A46,A48,TARSKI:def 4; end; then consider H being strict Subgroup of G such that A49: the carrier of H = E by A30,A31,GROUP_2:61; A50: now assume a in H; then a in E by A49,RLVECT_1:def 1; then consider Z being set such that A51: a in Z and A52: Z in C by TARSKI:def 4; consider D being Subset of G such that A53: Z = D and A54: ex H being strict Subgroup of G st H in Y & D = carr H by A52; consider H1 being strict Subgroup of G such that A55: H1 in Y & D = carr H1 by A54; not a in H1 by A6,A23,A55; hence contradiction by A51,A53,A55,GROUP_2:88; end; the carrier of H = carr H by GROUP_2:def 9; then reconsider y = H as Element of X by A6,A29,A49,A50; take y; let x be Element of X; assume A56: x in Y; x in Subgroups G by A5,TARSKI:def 3; then reconsider K = x as strict Subgroup of G by GROUP_3:def 1; take K,H; thus x = K & y = H; carr K = the carrier of K by GROUP_2:def 9; then the carrier of K in C by A56; then the carrier of K c= E by ZFMISC_1:92; hence K is Subgroup of H by A49,GROUP_2:66; end; hence thesis; end; consider s being Element of X such that A57: for y being Element of X st s <> y holds not P[s,y] from Zorn_Max(A17,A18,A19,A22); reconsider H = s as strict Subgroup of G by A16; H is maximal proof not a in H by A6; hence the HGrStr of H <> the HGrStr of G by RLVECT_1:def 1; let K be strict Subgroup of G; assume that A58: K <> the HGrStr of H and A59: H is Subgroup of K and A60: K <> the HGrStr of G; the carrier of H = carr H & the carrier of K = carr K & the carrier of H c= the carrier of K & M c= carr H by A6,A59,GROUP_2:def 5,def 9; then A61: M c= carr K by XBOOLE_1:1; now assume a in K; then a in carr K by GROUP_2:88; then {a} c= carr K by ZFMISC_1:37; then A62: M \/ {a} c= carr K by A61,XBOOLE_1:8; B c= M \/ {a} proof let x; assume A63: x in B; now per cases; suppose x = a; then x in {a} by TARSKI:def 1; hence thesis by XBOOLE_0:def 2; suppose x <> a; then not x in {a} by TARSKI:def 1; then x in M by A63,XBOOLE_0:def 4; hence thesis by XBOOLE_0:def 2; end; hence thesis; end; then B c= carr K by A62,XBOOLE_1:1; then gr B is Subgroup of gr carr K by Th41; then G is Subgroup of K by A3,Th40; hence contradiction by A60,GROUP_2:64; end; then reconsider v = K as Element of X by A6,A61; not P[s,v] by A57,A58; hence thesis by A59; end; then Phi(G) is Subgroup of H by Th54; then the carrier of Phi(G) c= the carrier of H by GROUP_2:def 5; then x in H & not a in H by A1,A6,RLVECT_1:def 1; hence thesis; end; let x; assume x in A; then consider a being Element of G such that A64: x = a and A65: a is non generating; now per cases; suppose for H being strict Subgroup of G holds H is not maximal; then Phi(G) = G by Def8; hence thesis by A64; suppose A66: ex H being strict Subgroup of G st H is maximal; now let H be strict Subgroup of G; assume A67: H is maximal; now assume A68: not a in H; then A69: gr(carr H \/ {a}) = G by A67,Th48; A70: carr H misses {a} proof thus carr H /\ {a} c= {} proof let x; assume x in carr H /\ {a}; then x in carr H & x in {a} by XBOOLE_0:def 3; then x in carr H & x = a by TARSKI:def 1; hence thesis by A68,GROUP_2:88; end; thus {} c= carr H /\ {a} by XBOOLE_1:2; end; (carr H \/ {a}) \ {a} = carr H \ {a} by XBOOLE_1:40 .= carr H by A70,XBOOLE_1:83; then gr((carr H \/ {a}) \ {a}) = H & H <> G by A67,Def7,Th40; hence contradiction by A65,A69,Def6; end; hence a in H; end; then a in Phi(G) by A66,Th52; hence thesis by A64,RLVECT_1:def 1; end; hence thesis; end; theorem for G being strict Group, a being Element of G holds a in Phi(G) iff a is non generating proof let G be strict Group, a be Element of G; thus a in Phi(G) implies a is non generating proof assume a in Phi(G); then a in the carrier of Phi(G) by RLVECT_1:def 1; then a in {b where b is Element of G: b is non generating} by Th55; then ex b being Element of G st a = b & b is non generating; hence thesis; end; assume a is non generating; then a in {b where b is Element of G : b is non generating}; then a in the carrier of Phi(G) by Th55; hence thesis by RLVECT_1:def 1; end; definition let G,H1,H2; func H1 * H2 -> Subset of G equals :Def9: carr H1 * carr H2; correctness; end; theorem Th57: H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 & H1 * H2 = carr H1 * H2 proof thus H1 * H2 = carr H1 * carr H2 by Def9; hence thesis by GROUP_2:def 11,def 12; end; theorem H * H = carr H proof thus H * H = carr H * carr H by Def9 .= carr H by GROUP_2:91; end; theorem H1 * H2 * H3 = H1 * (H2 * H3) proof thus H1 * H2 * H3 = carr H1 * carr H2 * H3 by Def9 .= carr H1 * (carr H2 * H3) by GROUP_2:116 .= carr H1 * (H2 * H3) by Th57 .= H1 * (H2 * H3) by GROUP_2:def 12; end; theorem a * H1 * H2 = a * (H1 * H2) proof thus a * H1 * H2 = a * carr H1 * H2 by GROUP_2:def 13 .= a * (carr H1 * H2) by GROUP_3:9 .= a * (H1 * H2) by Th57; end; theorem H1 * H2 * a = H1 * (H2 * a) proof thus H1 * H2 * a = H1 * carr H2 * a by Th57 .= H1 * (carr H2 * a) by GROUP_3:14 .= H1 * (H2 * a) by GROUP_2:def 14; end; theorem A * H1 * H2 = A * (H1 * H2) proof thus A * H1 * H2 = A * (H1 * carr H2) by GROUP_2:119 .= A * (H1 * H2) by Th57; end; theorem H1 * H2 * A = H1 * (H2 * A) proof thus H1 * H2 * A = H1 * carr H2 * A by Th57 .= H1 * (carr H2 * A) by GROUP_2:118 .= H1 * (H2 * A) by GROUP_2:def 12; end; theorem Th64: for N1,N2 being strict normal Subgroup of G holds N1 * N2 = N2 * N1 proof let N1,N2 be strict normal Subgroup of G; carr N1 * carr N2 = carr N2 * carr N1 by GROUP_3:148; then N1 * N2 = carr N2 * carr N1 by Def9; hence thesis by Def9; end; theorem Th65: G is commutative Group implies H1 * H2 = H2 * H1 proof assume G is commutative Group; then carr H1 * carr H2 = carr H2 * carr H1 by GROUP_2:29; then H1 * H2 = carr H2 * carr H1 by Def9; hence thesis by Def9; end; definition let G,H1,H2; func H1 "\/" H2 -> strict Subgroup of G equals :Def10: gr(carr H1 \/ carr H2); correctness; end; canceled; theorem Th67: a in H1 "\/" H2 iff ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I) proof thus a in H1 "\/" H2 implies ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I) proof assume a in H1 "\/" H2; then a in gr(carr H1 \/ carr H2) by Def10; hence thesis by Th37; end; assume ex F,I st len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I); then a in gr(carr H1 \/ carr H2) by Th37; hence thesis by Def10; end; Lm4: for n being natural number holds n mod 2 = 0 or n mod 2 = 1 proof let n be natural number; assume A1: n mod 2 <> 0; 2 = 1 + 1 & n mod 2 < 2 by NAT_1:46; then n mod 2 <= 1 & n mod 2 >= 1 by A1,NAT_1:38,RLVECT_1:98; hence n mod 2 = 1 by AXIOMS:21; end; Lm5: for k, n being Nat holds (k * n) mod k = 0 proof let k, n be Nat; now per cases; suppose k = 0; hence thesis by NAT_1:def 2; suppose k <> 0; then k * n = k * n + 0 & 0 < k by NAT_1:18; hence thesis by NAT_1:def 2; end; hence thesis; end; Lm6: for k, l being natural number holds k > 1 implies 1 mod k = 1 proof let k, l be natural number; assume A1: k > 1; 1 = k * 0 + 1; hence thesis by A1,NAT_1:def 2; end; Lm7: for k, l, n, m being natural number holds k mod n = 0 & l = k - m * n implies l mod n = 0 proof let k, l, n, m be natural number; assume that A1: k mod n = 0 and A2: l = k - m * n; now per cases; suppose n = 0; hence thesis by A1,A2; suppose n <> 0; then consider t being Nat such that A3: k = n * t + 0 and A4: 0 < n by A1,NAT_1:def 2; A5: l = n * (t - m) + 0 by A2,A3,XCMPLX_1:40; now assume t - m < 0; then l < n * 0 by A4,A5,REAL_1:70; hence contradiction by NAT_1:18; end; then t - m is Nat by INT_1:16; hence thesis by A4,A5,NAT_1:def 2; end; hence thesis; end; Lm8: n <> 0 & k mod n = 0 & l < n implies k + l mod n = l proof assume that A1: n <> 0 and A2: k mod n = 0 and A3: l < n; consider t being Nat such that A4: k = n * t + 0 and 0 < n by A1,A2,NAT_1:def 2; thus thesis by A3,A4,NAT_1:def 2; end; Lm9: k mod n = 0 implies k + l mod n = l mod n proof assume that A1: k mod n = 0; now per cases; suppose A2: n = 0; hence k + l mod n = 0 by NAT_1:def 2 .= l mod n by A2,NAT_1:def 2; suppose A3: n <> 0; then consider m such that A4: k = n * m + 0 & 0 < n by A1,NAT_1:def 2; consider t being Nat such that A5: l = n * t + (l mod n) & l mod n < n by A3,NAT_1:def 2; k + l = n * m + n * t + (l mod n) by A4,A5,XCMPLX_1:1 .= n * (m + t) + (l mod n) by XCMPLX_1:8; hence thesis by A5,NAT_1:def 2; end; hence thesis; end; Lm10: k <> 0 implies (k * n) div k = n proof assume k <> 0; then k * n = k * n + 0 & 0 < k by NAT_1:18; hence thesis by NAT_1:def 1; end; Lm11: n <> 0 & k mod n = 0 implies (k + l) div n = (k div n) + (l div n) proof assume that A1:n <> 0 and A2: k mod n = 0; A3: 0 <= n by NAT_1:18; then A4: k = n * (k div n) + 0 by A1,A2,NAT_1:47; A5: ex t being Nat st l = n * t + (l mod n) & l mod n < n by A1,NAT_1:def 2; l = n * (l div n) + (l mod n) by A1,A3,NAT_1:47; then k + l = n * (k div n) + n * (l div n) + (l mod n) by A4,XCMPLX_1:1 .= n * ((k div n) + (l div n)) + (l mod n) by XCMPLX_1:8; hence thesis by A5,NAT_1:def 1; end; theorem H1 "\/" H2 = gr(H1 * H2) proof set H = gr(carr H1 * carr H2); A1: carr H1 * carr H2 = H1 * H2 by Def9; A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10; carr H1 \/ carr H2 c= carr H1 * carr H2 proof let x; assume A3: x in carr H1 \/ carr H2; then reconsider a = x as Element of G; now per cases by A3,XBOOLE_0:def 2; suppose A4: x in carr H1; 1.G in H2 by GROUP_2:55; then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88; hence thesis by A4,GROUP_2:12; suppose A5: x in carr H2; 1.G in H1 by GROUP_2:55; then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88; hence thesis by A5,GROUP_2:12; end; hence thesis; end; then A6: H1 "\/" H2 is Subgroup of H by A2,Th41; now let a; assume a in H; then consider F,I such that A7: len F = len I and A8: rng F c= carr H1 * carr H2 and A9: a = Product(F |^ I) by Th37; rng(F |^ I) c= carr(H1 "\/" H2) proof let x; set f = F |^ I; assume x in rng f; then consider y such that A10: y in dom f and A11: f.y = x by FUNCT_1:def 5; reconsider y as Nat by A10; A12: len f = len F by Def4; then A13: y in dom I by A7,A10,FINSEQ_3:31; then I.y in rng I & rng I c= INT by FINSEQ_1:def 4,FUNCT_1:def 5; then reconsider i = I.y as Integer by INT_1:12; A14: y in dom F by A10,A12,FINSEQ_3:31; I/.y = I.y & @(I/.y) = I/.y by A13,Def2,FINSEQ_4:def 4; then A15: x = (F/.y) |^ i by A11,A14,Def4; y in dom F by A10,A12,FINSEQ_3:31; then F/.y = F.y & F.y in rng F by FINSEQ_4:def 4,FUNCT_1:def 5; then consider b,c such that A16: F/.y = b * c and A17: b in carr H1 and A18: c in carr H2 by A8,GROUP_2:12; now per cases; suppose i >= 0; then reconsider n = i as Nat by INT_1:16; defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = b) & ($1 mod 2 = 0 implies $2 = c); A19: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds y1 = y2 by Lm4; A20: for k st k in Seg(2 * n) ex x st P[k,x] proof let k; assume k in Seg(2 * n); now per cases by Lm4; suppose A21: k mod 2 = 1; reconsider x = b as set; take x; thus (k mod 2 = 1 implies x = b) & (k mod 2 = 0 implies x = c) by A21; suppose A22: k mod 2 = 0; reconsider x = c as set; take x; thus (k mod 2 = 1 implies x = b) & (k mod 2 = 0 implies x = c) by A22; end; hence thesis; end; consider p being FinSequence such that A23: dom p = Seg(2 * n) and A24: for k st k in Seg(2 * n) holds P[k,p.k] from SeqEx(A19,A20 ); A25: len p = 2 * n by A23,FINSEQ_1:def 3; A26: rng p c= {b,c} proof let x; assume x in rng p; then consider y such that A27: y in dom p and A28: p.y = x by FUNCT_1:def 5; reconsider y as Nat by A27; now per cases by Lm4; suppose y mod 2 = 0; then x = c by A23,A24,A27,A28; hence thesis by TARSKI:def 2; suppose y mod 2 = 1; then x = b by A23,A24,A27,A28; hence thesis by TARSKI:def 2; end; hence thesis; end; then rng p c= the carrier of G by XBOOLE_1:1; then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4; defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies for F1 st F1 = p | Seg $1 holds Product(F1) = (F/.y) |^ ($1 div 2); A29: for k st for l st l < k holds Q[l] holds Q[k] proof let k; assume A30: for l st l < k holds Q[l]; assume that A31: k <= 2 * n and A32: k mod 2 = 0; let F1; assume A33: F1 = p | Seg k; now per cases; suppose A34: k = 0; then F1 = <*> the carrier of G by A33,FINSEQ_1:4, RELAT_1:110; then A35: Product F1 = 1.G by Th11; 2 * 0 = 0; then 0 div 2 = 0 by Lm10; hence thesis by A34,A35,GROUP_1:43; suppose k <> 0; then A36: k >= 1 by RLVECT_1:98; k <> 1 by A32,Lm6; then k > 1 by A36,REAL_1:def 5; then k >= 1 + 1 by NAT_1:38; then k - 2 >= 2 - 2 by REAL_1:49; then reconsider m = k - 2 as Nat by INT_1:16; A37: m + 2 = k by XCMPLX_1:27; then A38: m < k by RLVECT_1:102; then A39: m <= 2 * n by A31,AXIOMS:22; 1 * 2 = 2; then A40: m mod 2 = 0 by A32,Lm7; reconsider q = p | Seg m as FinSequence of the carrier of G by FINSEQ_1:23; A41: Product q = (F/.y) |^ (m div 2) by A30,A38,A39,A40; A42: ex j being Nat st 2 * n = k + j by A31,NAT_1:28; ex o being Nat st 2 * n = m + o by A39,NAT_1:28; then A43: len F1 = k & len q = m by A25,A33,A42,FINSEQ_3:59; then A44: len F1 = m + 2 by XCMPLX_1:27 .= len q + len<* b,c *> by A43,FINSEQ_1:61; A45: now let l; assume A46: l in dom q; then 1 <= l & l <= len q & len q <= len F1 by A37,A43,FINSEQ_3:27,RLVECT_1:102 ; then 1 <= l & l <= len F1 by AXIOMS:22; then l in dom F1 by FINSEQ_3:27; then F1.l = p.l & q.l = p.l by A33,A46,FUNCT_1:70; hence F1.l = q.l; end; now let l; assume l in dom<* b,c *>; then A47: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29; now per cases by A47,TARSKI:def 2; suppose A48: l = 1; then A49: <* b,c *>.l = b by FINSEQ_1:61; m + 1 <= k & 1 <= m + 1 by A38,NAT_1:37,38; then A50: m + 1 in dom F1 by A43,FINSEQ_3:27; then A51: F1.(len q + l) = p.(m + 1) by A33,A43, A48,FUNCT_1:70; A52: m + 1 mod 2 = 1 by A40,Lm8; dom F1 c= dom p by A33,FUNCT_1:76; hence F1.(len q + l) = <* b,c *>.l by A23,A24, A49,A50,A51,A52; suppose A53: l = 2; then A54: <* b,c *>.l = c by FINSEQ_1:61; 1 <= m + (1 + 1) by NAT_1:37; then A55: m + 2 in dom F1 by A37,A43,FINSEQ_3:27; then A56: F1.(len q + l) = p.(m + 2) by A33,A43, A53,FUNCT_1:70; 2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5; then A57: m + 2 mod 2 = 0 by A40,Lm9; dom F1 c= dom p by A33,FUNCT_1:76; hence F1.(len q + l) = <* b,c *>.l by A23,A24, A54,A55,A56,A57; end; hence F1.(len q + l) = <* b,c *>.l; end; then F1 = q ^ <* b,c *> by A44,A45,FINSEQ_3:43; then A58: Product F1 = Product q * Product<* b,c *> by Th8 .= Product q * (F/.y) by A16,Th13 .= (F/.y) |^ ((m div 2) + 1) by A41,GROUP_1:49; m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10 .= k div 2 by A37,A40,Lm11; hence thesis by A58; end; hence thesis; end; A59: for k holds Q[k] from Comp_Ind(A29); A60: 2 * n mod 2 = 0 by Lm5; A61: 2 * n div 2 = n by Lm10; len p = 2 * n by A23,FINSEQ_1:def 3; then p = p | Seg(2 * n) by FINSEQ_3:55; then A62: x = Product(p) by A15,A59,A60,A61; b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A17,A18, XBOOLE_0:def 2; then {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38; then A63: rng p c= carr H1 \/ carr H2 by A26,XBOOLE_1:1; carr H1 \/ carr H2 c= the carrier of gr(carr H1 \/ carr H2) & carr gr(carr H1 \/ carr H2) = the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9; then rng p c= carr gr(carr H1 \/ carr H2) by A63,XBOOLE_1:1; then x in gr(carr H1 \/ carr H2) by A62,Th21; then x in H1 "\/" H2 by Def10; hence thesis by GROUP_2:88; suppose A64: i < 0; set n = abs( i ); defpred P[Nat,set] means ($1 mod 2 = 1 implies $2 = c") & ($1 mod 2 = 0 implies $2 = b"); A65: for k,y1,y2 st k in Seg(2 * n) & P[k,y1] & P[k,y2] holds y1 = y2 by Lm4; A66: for k st k in Seg(2 * n) ex x st P[k,x] proof let k; assume k in Seg(2 * n); now per cases by Lm4; suppose A67: k mod 2 = 1; reconsider x = c" as set; take x; thus (k mod 2 = 1 implies x = c") & (k mod 2 = 0 implies x = b") by A67; suppose A68: k mod 2 = 0; reconsider x = b" as set; take x; thus (k mod 2 = 1 implies x = c") & (k mod 2 = 0 implies x = b") by A68; end; hence thesis; end; consider p being FinSequence such that A69: dom p = Seg(2 * n) and A70: for k st k in Seg(2 * n) holds P[k,p.k] from SeqEx(A65,A66); A71: len p = 2 * n by A69,FINSEQ_1:def 3; A72: rng p c= {b",c"} proof let x; assume x in rng p; then consider y such that A73: y in dom p and A74: p.y = x by FUNCT_1:def 5; reconsider y as Nat by A73; now per cases by Lm4; suppose y mod 2 = 0; then x = b" by A69,A70,A73,A74; hence thesis by TARSKI:def 2; suppose y mod 2 = 1; then x = c" by A69,A70,A73,A74; hence thesis by TARSKI:def 2; end; hence thesis; end; then rng p c= the carrier of G by XBOOLE_1:1; then reconsider p as FinSequence of the carrier of G by FINSEQ_1:def 4; defpred Q[Nat] means $1 <= 2 * n & $1 mod 2 = 0 implies for F1 st F1 = p | Seg $1 holds Product(F1) = ((F/.y) |^ ($1 div 2))"; A75: for k st for l st l < k holds Q[l] holds Q[k] proof let k; assume A76: for l st l < k holds Q[l]; assume that A77: k <= 2 * n and A78: k mod 2 = 0; let F1; assume A79: F1 = p | Seg k; now per cases; suppose A80: k = 0; then F1 = <*> the carrier of G by A79,FINSEQ_1:4, RELAT_1:110; then A81: Product F1 = 1.G by Th11; 2 * 0 = 0; then 0 div 2 = 0 by Lm10; then (F/.y) |^ (k div 2) = 1.G by A80,GROUP_1:43; hence thesis by A81,GROUP_1:16; suppose k <> 0; then A82: k >= 1 by RLVECT_1:98; k <> 1 by A78,Lm6; then k > 1 by A82,REAL_1:def 5; then k >= 1 + 1 by NAT_1:38; then k - 2 >= 2 - 2 by REAL_1:49; then reconsider m = k - 2 as Nat by INT_1:16; A83: m + 2 = k by XCMPLX_1:27; then A84: m < k by RLVECT_1:102; then A85: m <= 2 * n by A77,AXIOMS:22; 1 * 2 = 2; then A86: m mod 2 = 0 by A78,Lm7; reconsider q = p | Seg m as FinSequence of the carrier of G by FINSEQ_1:23; A87: Product q = ((F/.y) |^ (m div 2))" by A76,A84,A85,A86; A88: ex j being Nat st 2 * n = k + j by A77,NAT_1:28; ex o being Nat st 2 * n = m + o by A85,NAT_1:28; then A89: len F1 = k & len q = m by A71,A79,A88,FINSEQ_3:59; then A90: len F1 = m + 2 by XCMPLX_1:27 .= len q + len<* c",b" *> by A89,FINSEQ_1:61; A91: now let l; assume A92: l in dom q; then 1 <= l & l <= len q & len q <= len F1 by A83,A89,FINSEQ_3:27,RLVECT_1:102 ; then 1 <= l & l <= len F1 by AXIOMS:22; then l in dom F1 by FINSEQ_3:27; then F1.l = p.l & q.l = p.l by A79,A92,FUNCT_1:70; hence F1.l = q.l; end; now let l; assume l in dom<* c",b" *>; then A93: l in {1,2} by FINSEQ_1:4,FINSEQ_3:29; now per cases by A93,TARSKI:def 2; suppose A94: l = 1; then A95: <* c",b" *>.l = c" by FINSEQ_1:61; m + 1 <= k & 1 <= m + 1 by A84,NAT_1:37,38; then A96: m + 1 in dom F1 by A89,FINSEQ_3:27; then A97: F1.(len q + l) = p.(m + 1) by A79,A89, A94,FUNCT_1:70; A98: m + 1 mod 2 = 1 by A86,Lm8; dom F1 c= dom p by A79,FUNCT_1:76; hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A95,A96,A97,A98; suppose A99: l = 2; then A100: <* c",b" *>.l = b" by FINSEQ_1:61; 1 <= m + (1 + 1) by NAT_1:37; then A101: m + 2 in dom F1 by A83,A89,FINSEQ_3:27 ; then A102: F1.(len q + l) = p.(m + 2) by A79,A89 ,A99,FUNCT_1:70; 2 * 1 = 2 & 2 * 1 mod 2 = 0 by Lm5; then A103: m + 2 mod 2 = 0 by A86,Lm9; dom F1 c= dom p by A79,FUNCT_1:76; hence F1.(len q + l) = <* c",b" *>.l by A69,A70,A100,A101,A102,A103; end; hence F1.(len q + l) = <* c",b" *>.l; end; then F1 = q ^ <* c",b" *> by A90,A91,FINSEQ_3:43; then A104: Product F1 = Product q * Product<* c",b" *> by Th8 .= Product q * (c" * b") by Th13 .= Product q * (F/.y)" by A16,GROUP_1:25 .= ((F/.y) * ((F/.y) |^ (m div 2)))" by A87,GROUP_1:25 .= ((F/.y) |^ ((m div 2) + 1))" by GROUP_1:49; m div 2*1 + 1 = (m div 2) + (2 div 2) by Lm10 .= k div 2 by A83,A86,Lm11; hence thesis by A104; end; hence thesis; end; A105: for k holds Q[k] from Comp_Ind(A75); A106: 2 * n mod 2 = 0 by Lm5; A107: 2 * n div 2 = n by Lm10; len p = 2 * n by A69,FINSEQ_1:def 3; then A108: p = p | Seg(2 * n) by FINSEQ_3:55; x = ((F/.y) |^ n)" by A15,A64,GROUP_1:56; then A109: x = Product(p) by A105,A106,A107,A108; b" in carr H1 & c" in carr H2 by A17,A18,GROUP_2:90; then b" in carr H1 \/ carr H2 & c" in carr H1 \/ carr H2 by XBOOLE_0:def 2; then {b",c"} c= carr H1 \/ carr H2 by ZFMISC_1:38; then A110: rng p c= carr H1 \/ carr H2 by A72,XBOOLE_1:1; carr H1 \/ carr H2 c= the carrier of gr(carr H1 \/ carr H2) & carr gr(carr H1 \/ carr H2) = the carrier of gr(carr H1 \/ carr H2) by Def5,GROUP_2:def 9; then rng p c= carr gr(carr H1 \/ carr H2) by A110,XBOOLE_1:1; then x in gr(carr H1 \/ carr H2) by A109,Th21; then x in H1 "\/" H2 by Def10; hence thesis by GROUP_2:88; end; hence thesis; end; hence a in H1 "\/" H2 by A9,Th21; end; then H is Subgroup of H1 "\/" H2 by GROUP_2:67; hence gr(H1 * H2) = H1 "\/" H2 by A1,A6,GROUP_2:64; end; theorem Th69: H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2 proof assume H1 * H2 = H2 * H1; then carr H1 * carr H2 = H2 * H1 by Def9; then carr H1 * carr H2 = carr H2 * carr H1 by Def9; then consider H being strict Subgroup of G such that A1: the carrier of H = carr H1 * carr H2 by GROUP_2:93; A2: H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10; carr H1 \/ carr H2 c= carr H1 * carr H2 proof let x; assume A3: x in carr H1 \/ carr H2; then reconsider a = x as Element of G; now per cases by A3,XBOOLE_0:def 2; suppose A4: x in carr H1; 1.G in H2 by GROUP_2:55; then 1.G in carr H2 & a * 1.G = a by GROUP_1:def 4,GROUP_2:88; hence thesis by A4,GROUP_2:12; suppose A5: x in carr H2; 1.G in H1 by GROUP_2:55; then 1.G in carr H1 & 1.G * a = a by GROUP_1:def 4,GROUP_2:88; hence thesis by A5,GROUP_2:12; end; hence thesis; end; then A6: H1 "\/" H2 is Subgroup of H by A1,A2,Def5; now let a; assume a in H; then a in carr H1 * carr H2 by A1,RLVECT_1:def 1; then consider b,c such that A7: a = b * c and A8: b in carr H1 & c in carr H2 by GROUP_2:12; reconsider p = 1 as Integer; A9: len<* b,c *> = 2 & len<* @p,@p *> = 2 by FINSEQ_1:61; A10: rng<* b,c *> = {b,c} by FINSEQ_2:147; b in carr H1 \/ carr H2 & c in carr H1 \/ carr H2 by A8,XBOOLE_0:def 2 ; then A11: {b,c} c= carr H1 \/ carr H2 by ZFMISC_1:38; a = Product<* b *> * c by A7,Th12 .= Product<* b *> * Product<* c *> by Th12 .= Product(<* b *> ^ <* c *>) by Th8 .= Product<* b,c *> by FINSEQ_1:def 9 .= Product<* b |^ p, c *> by GROUP_1:44 .= Product<* b |^ p, c |^ p *> by GROUP_1:44 .= Product(<* b,c *> |^ <* @p,@p *>) by Th29; then a in gr(carr H1 \/ carr H2) by A9,A10,A11,Th37; hence a in H1 "\/" H2 by Def10; end; then H is Subgroup of H1 "\/" H2 by GROUP_2:67; then H = H1 "\/" H2 & carr H1 * carr H2 = H1 * H2 by A6,Def9,GROUP_2:64; hence thesis by A1; end; theorem G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2 proof assume G is commutative Group; then H1 * H2 = H2 * H1 by Th65; hence thesis by Th69; end; theorem Th71: for N1,N2 being strict normal Subgroup of G holds the carrier of N1 "\/" N2 = N1 * N2 proof let N1,N2 be strict normal Subgroup of G; N1 * N2 = N2 * N1 by Th64; hence thesis by Th69; end; theorem for N1,N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G proof let N1,N2 be strict normal Subgroup of G; consider N being strict normal Subgroup of G such that A1: the carrier of N = carr N1 * carr N2 by GROUP_3:149; the carrier of N1 "\/" N2 = N1 * N2 & N1 * N2 = carr N1 * carr N2 by Th57,Th71; hence thesis by A1,GROUP_2:68; end; theorem Th73: for H being strict Subgroup of G holds H "\/" H = H proof let H be strict Subgroup of G; thus H "\/" H = gr(carr H \/ carr H) by Def10 .= H by Th40; end; theorem Th74: H1 "\/" H2 = H2 "\/" H1 proof thus H1 "\/" H2 = gr(carr H2 \/ carr H1) by Def10 .= H2 "\/" H1 by Def10; end; Lm12: H1 is Subgroup of H1 "\/" H2 proof carr H1 c= carr H1 \/ carr H2 & carr H1 \/ carr H2 c= the carrier of gr(carr H1 \/ carr H2) & H1 "\/" H2 = gr(carr H1 \/ carr H2) & the carrier of H1 = carr H1 by Def5,Def10,GROUP_2:def 9,XBOOLE_1:7; then the carrier of H1 c= the carrier of H1 "\/" H2 by XBOOLE_1:1; hence thesis by GROUP_2:66; end; Lm13: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) proof now let a; assume a in H1 "\/" H2 "\/" H3; then consider F,I such that A1: len F = len I and A2: rng F c= carr(H1 "\/" H2) \/ carr H3 and A3: a = Product(F |^ I) by Th67; rng F c= carr gr(carr H1 \/ carr(H2 "\/" H3)) proof let x; assume A4: x in rng F; now per cases by A2,A4,XBOOLE_0:def 2; suppose A5: x in carr(H1 "\/" H2); then A6: x in H1 "\/" H2 by GROUP_2:88; reconsider b = x as Element of G by A5; consider F1,I1 such that A7: len F1 = len I1 and A8: rng F1 c= carr H1 \/ carr H2 and A9: b = Product(F1 |^ I1) by A6,Th67; H2 is Subgroup of H2 "\/" H3 by Lm12; then the carrier of H2 c= the carrier of H2 "\/" H3 & the carrier of H2 = carr H2 & the carrier of H3 = carr H3 & H2 "\/" H3 = gr(carr H2 \/ carr H3) by Def10,GROUP_2:def 5,def 9; then carr H2 c= carr(H2 "\/" H3) by GROUP_2:def 9; then carr H1 \/ carr H2 c= carr H1 \/ carr(H2 "\/" H3) by XBOOLE_1:9; then rng F1 c= carr H1 \/ carr(H2 "\/" H3) by A8,XBOOLE_1:1; then b in H1 "\/" (H2 "\/" H3) by A7,A9,Th67; then x in gr(carr H1 \/ carr(H2 "\/" H3)) by Def10; hence thesis by GROUP_2:88; suppose x in carr H3; then x in H3 & H3 is Subgroup of H3 "\/" H2 by Lm12,GROUP_2:88; then x in H3 "\/" H2 by GROUP_2:49; then x in H2 "\/" H3 by Th74; then x in carr(H2 "\/" H3) by GROUP_2:88; then x in carr H1 \/ carr(H2 "\/" H3) & carr H1 \/ carr(H2 "\/" H3) c= the carrier of gr(carr H1 \/ carr(H2 "\/" H3)) by Def5,XBOOLE_0:def 2 ; then x in the carrier of gr(carr H1 \/ carr(H2 "\/" H3)); hence thesis by GROUP_2:def 9; end; hence thesis; end; then a in gr carr gr(carr H1 \/ carr(H2 "\/" H3)) by A1,A3,Th37; then a in gr(carr H1 \/ carr(H2 "\/" H3)) by Th40; hence a in H1 "\/" (H2 "\/" H3) by Def10; end; hence thesis by GROUP_2:67; end; theorem Th75: H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3) proof A1: H1 "\/" H2 "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm13; H2 "\/" H3 "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) by Lm13; then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" H1 "\/" H2 & H3 "\/" H1 "\/" H2 is Subgroup of H3 "\/" (H1 "\/" H2) by Lm13,Th74; then H2 "\/" H3 "\/" H1 is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:65; then H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by Th74; then H1 "\/" (H2 "\/" H3) is Subgroup of H1 "\/" H2 "\/" H3 by Th74; hence thesis by A1,GROUP_2:64; end; theorem for H being strict Subgroup of G holds (1).G "\/" H = H & H "\/" (1).G = H proof let H be strict Subgroup of G; A1: carr(1).G = the carrier of (1).G by GROUP_2:def 9 .= {1.G} by GROUP_2:def 7; 1.G in H by GROUP_2:55; then 1.G in carr H by GROUP_2:88; then {1.G} c= carr H by ZFMISC_1:37; then A2: {1.G} \/ carr H = carr H by XBOOLE_1:12; thus (1).G "\/" H = gr(carr(1).G \/ carr H) by Def10 .= H by A1,A2,Th40; hence thesis by Th74; end; theorem Th77: (Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G proof A1: [#] the carrier of G = the carrier of the HGrStr of G by SUBSET_1:def 4 .= the carrier of (Omega).G by GROUP_2:def 8; A2: carr (Omega).G = the carrier of (Omega).G by GROUP_2:def 9; (the carrier of (Omega). G) \/ carr H = [#] the carrier of G by A1,SUBSET_1:28; hence (Omega).G "\/" H = gr carr (Omega).G by A1,A2,Def10 .= (Omega).G by Th40; hence thesis by Th74; end; theorem Th78: H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 proof H1 "\/" H2 = H2 "\/" H1 by Th74; hence thesis by Lm12; end; theorem Th79: for H2 being strict Subgroup of G holds H1 is Subgroup of H2 iff H1 "\/" H2 = H2 proof let H2 be strict Subgroup of G; thus H1 is Subgroup of H2 implies H1 "\/" H2 = H2 proof assume H1 is Subgroup of H2; then A1: the carrier of H1 c= the carrier of H2 & the carrier of H1 = carr H1 & carr H2 = the carrier of H2 by GROUP_2:def 5,def 9; thus H1 "\/" H2 = gr(carr H1 \/ carr H2) by Def10 .= gr carr H2 by A1,XBOOLE_1:12 .= H2 by Th40; end; thus thesis by Th78; end; theorem H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3 proof H2 is Subgroup of H2 "\/" H3 by Th78; hence thesis by GROUP_2:65; end; theorem 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 proof let H3 be strict Subgroup of G; assume that A1: H1 is Subgroup of H3 and A2: H2 is Subgroup of H3; now let a; assume a in H1 "\/" H2; then consider F,I such that A3: len F = len I & rng F c= carr H1 \/ carr H2 & a = Product(F |^ I) by Th67; the carrier of H1 c= the carrier of H3 & the carrier of H2 c= the carrier of H3 & the carrier of H1 = carr H1 & the carrier of H2 = carr H2 & the carrier of H3 = carr H3 by A1,A2,GROUP_2:def 5,def 9; then carr H1 \/ carr H2 c= carr H3 by XBOOLE_1:8; then rng F c= carr H3 by A3,XBOOLE_1:1; then a in gr carr H3 by A3,Th37; hence a in H3 by Th40; end; hence thesis by GROUP_2:67; end; theorem for H3,H2 being strict Subgroup of G holds H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3 proof let H3,H2 be strict Subgroup of G; assume A1: H1 is Subgroup of H2; (H1 "\/" H3) "\/" (H2 "\/" H3) = H1 "\/" H3 "\/" H2 "\/" H3 by Th75 .= H1 "\/" (H3 "\/" H2) "\/" H3 by Th75 .= H1 "\/" (H2 "\/" H3) "\/" H3 by Th74 .= H1 "\/" H2 "\/" H3 "\/" H3 by Th75 .= H2 "\/" H3 "\/" H3 by A1,Th79 .= H2 "\/" (H3 "\/" H3) by Th75 .= H2 "\/" H3 by Th73; hence thesis by Th79; end; theorem H1 /\ H2 is Subgroup of H1 "\/" H2 proof H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2 by Th78,GROUP_2:106; hence thesis by GROUP_2:65; end; theorem Th84: for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2 proof let H2 be strict Subgroup of G; H1 /\ H2 is Subgroup of H2 by GROUP_2:106; hence thesis by Th79; end; theorem Th85: for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1 proof let H1 be strict Subgroup of G; H1 is Subgroup of H1 "\/" H2 by Th78; hence thesis by GROUP_2:107; end; theorem for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1 proof let H1,H2 be strict Subgroup of G; (H1 "\/" H2 = H2 iff H1 is Subgroup of H2) & (H1 /\ H2 = H1 iff H1 is Subgroup of H2) by Th79,GROUP_2:107; hence thesis; end; reserve S1,S2 for Element of Subgroups G; definition let G; func SubJoin G -> BinOp of Subgroups G means :Def11: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 "\/" H2; existence proof defpred P[set,set,set] means for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 "\/" H2; A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B] proof let S1,S2; reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1; reconsider C = H1 "\/" H2 as Element of Subgroups(G) by GROUP_3:def 1; take C; thus thesis; end; ex o being BinOp of Subgroups G st for a,b being Element of Subgroups G holds P[a,b,o.(a,b)] from BinOpEx(A1); hence thesis; end; uniqueness proof let o1,o2 be BinOp of Subgroups(G); assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 "\/" H2; assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 "\/" H2; now let x,y be set; assume A4: x in Subgroups(G) & y in Subgroups(G); then reconsider A = x, B = y as Element of Subgroups(G); reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1; o1.(A,B) = H1 "\/" H2 & o2.(A,B) = H1 "\/" H2 by A2,A3; then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y) by BINOP_1:def 1; hence o1.[x,y] = o2.[x,y]; end; hence thesis by FUNCT_2:118; end; end; definition let G; func SubMeet G -> BinOp of Subgroups G means :Def12: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds it.(S1,S2) = H1 /\ H2; existence proof defpred P[set,set,set] means for H1,H2 st $1 = H1 & $2 = H2 holds $3 = H1 /\ H2; A1: for S1,S2 ex B being Element of Subgroups G st P[S1,S2,B] proof let S1,S2; reconsider H1 = S1, H2 = S2 as Subgroup of G by GROUP_3:def 1; reconsider C = H1 /\ H2 as Element of Subgroups(G) by GROUP_3:def 1; take C; thus thesis; end; ex o being BinOp of Subgroups G st for a,b being Element of Subgroups G holds P[a,b,o.(a,b)] from BinOpEx(A1); hence thesis; end; uniqueness proof let o1,o2 be BinOp of Subgroups(G); assume A2: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o1.(S1,S2) = H1 /\ H2; assume A3: for S1,S2,H1,H2 st S1 = H1 & S2 = H2 holds o2.(S1,S2) = H1 /\ H2; now let x,y be set; assume A4: x in Subgroups(G) & y in Subgroups(G); then reconsider A = x, B = y as Element of Subgroups(G); reconsider H1 = x, H2 = y as Subgroup of G by A4,GROUP_3:def 1; o1.(A,B) = H1 /\ H2 & o2.(A,B) = H1 /\ H2 by A2,A3; then o1.(x,y) = o2.(x,y) & o1.[x,y] = o1.(x,y) & o2.[x,y] = o2.(x,y) by BINOP_1:def 1; hence o1.[x,y] = o2.[x,y]; end; hence thesis by FUNCT_2:118; end; end; Lm14: 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 proof let G be Group; set L = LattStr (# Subgroups G, SubJoin G, SubMeet G #); A1: now let A,B be Element of L; let H1,H2 be Subgroup of G; assume A2: A = H1 & B = H2; reconsider A'= A, B'= B as Element of Subgroups G; thus A "/\" B = SubMeet(G).(A',B') by LATTICES:def 2 .= H1 /\ H2 by A2,Def12; end; A3: now let A,B be Element of L; let H1,H2 be Subgroup of G; assume A4: A = H1 & B = H2; reconsider A'= A, B'= B as Element of Subgroups G; thus A "\/" B = SubJoin(G).(A',B') by LATTICES:def 1 .= H1 "\/" H2 by A4,Def11; end; now let A,B,C be Element of L; reconsider H1 = A, H2 = B, H3 = C as strict Subgroup of G by GROUP_3:def 1; thus A "\/" B = H1 "\/" H2 by A3 .= H2 "\/" H1 by Th74 .= B "\/" A by A3; A5: H1 "\/" H2 = A "\/" B & H2 "\/" H3 = B "\/" C by A3; hence A "\/" B "\/" C = H1 "\/" H2 "\/" H3 by A3 .= H1 "\/" (H2 "\/" H3) by Th75 .= A "\/" (B "\/" C) by A3,A5; A6: H1 /\ H2 = A "/\" B by A1; hence (A "/\" B) "\/" B = (H1 /\ H2) "\/" H2 by A3 .= B by Th84; thus A "/\" B = H2 /\ H1 by A1 .= B "/\" A by A1; A7: H2 /\ H3 = B "/\" C by A1; thus A "/\" B "/\" C = H1 /\ H2 /\ H3 by A1,A6 .= H1 /\ (H2 /\ H3) by GROUP_2:102 .= A "/\" (B "/\" C) by A1,A7; thus A "/\" (A "\/" B) = H1 /\ (H1 "\/" H2) by A1,A5 .= A by Th85; end; then A8: L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by LATTICES:def 4,def 5,def 6,def 7,def 8,def 9; hence L is Lattice by LATTICES:def 10; reconsider L as Lattice by A8,LATTICES:def 10; reconsider E = (1).G as Element of L by GROUP_3:def 1; now let A be Element of L; reconsider H = A as Subgroup of G by GROUP_3:def 1; thus E "/\" A = (1).G /\ H by A1 .= E by GROUP_2:103; hence A "/\" E = E; end; hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 0_Lattice by LATTICES:def 13; reconsider F = (Omega).G as Element of L by GROUP_3:def 1; now let A be Element of L; reconsider H = A as Subgroup of G by GROUP_3:def 1; thus F "\/" A = (Omega).G "\/" H by A3 .= F by Th77; hence A "\/" F = F; end; hence LattStr (# Subgroups G, SubJoin G, SubMeet G #) is 1_Lattice by LATTICES:def 14; end; definition let G be Group; func lattice G -> strict Lattice equals :Def13: LattStr (# Subgroups G, SubJoin G, SubMeet G #); coherence by Lm14; end; canceled 5; theorem Th92: for G being Group holds the carrier of lattice G = Subgroups G proof let G be Group; lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13; hence thesis; end; theorem Th93: for G being Group holds the L_join of lattice G = SubJoin G proof let G be Group; lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13; hence thesis; end; theorem Th94: for G being Group holds the L_meet of lattice G = SubMeet G proof let G be Group; lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13; hence thesis; end; definition let G be Group; cluster lattice G -> lower-bounded upper-bounded; coherence proof A1: lattice G = LattStr (# Subgroups G, SubJoin G, SubMeet G #) by Def13; hence lattice G is lower-bounded by Lm14; thus lattice G is upper-bounded by A1,Lm14; end; end; canceled 3; theorem for G being Group holds Bottom lattice G = (1).G proof let G be Group; A1: the carrier of lattice G = Subgroups G by Th92; set L = lattice G; reconsider E = (1).G as Element of L by A1,GROUP_3:def 1; now let A be Element of L; reconsider H = A as Subgroup of G by A1,GROUP_3:def 1; thus A "/\" E = (the L_meet of lattice G).(A,E) by LATTICES:def 2 .= SubMeet(G).(A,E) by Th94 .= H /\ (1).G by A1,Def12 .= E by GROUP_2:103; end; hence thesis by RLSUB_2:84; end; theorem for G being Group holds Top lattice G = (Omega).G proof let G be Group; A1: the carrier of lattice G = Subgroups G by Th92; set L = lattice G; reconsider E = (Omega). G as Element of L by A1,GROUP_3:def 1; now let A be Element of L; reconsider H = A as Subgroup of G by A1,GROUP_3:def 1; thus A "\/" E = (the L_join of lattice G).(A,E) by LATTICES:def 1 .= SubJoin(G).(A,E) by Th93 .= H "\/" (Omega).G by A1,Def11 .= E by Th77; end; hence thesis by RLSUB_2:85; end; :: :: Auxiliary theorems. :: reserve k, l, m, n for natural number; theorem n mod 2 = 0 or n mod 2 = 1 by Lm4; theorem for k, n being Nat holds (k * n) mod k = 0 by Lm5; theorem k > 1 implies 1 mod k = 1 by Lm6; theorem k mod n = 0 & l = k - m * n implies l mod n = 0 by Lm7; reserve k, n, l, m for Nat; theorem n <> 0 & k mod n = 0 & l < n implies k + l mod n = l by Lm8; theorem k mod n = 0 implies k + l mod n = l mod n by Lm9; theorem n <> 0 & k mod n = 0 implies (k + l) div n = (k div n) + (l div n) by Lm11; theorem k <> 0 implies (k * n) div k = n by Lm10;

Back to top