:: GROUP_8 semantic presentation begin theorem :: GROUP_8:1 for p being Element of NAT for G being finite strict Group st p is prime & card G = p holds ex a being Element of G st ord a = p proof let p be Element of NAT ; ::_thesis: for G being finite strict Group st p is prime & card G = p holds ex a being Element of G st ord a = p let G be finite strict Group; ::_thesis: ( p is prime & card G = p implies ex a being Element of G st ord a = p ) assume that A1: p is prime and A2: card G = p ; ::_thesis: ex a being Element of G st ord a = p G is cyclic Group by A1, A2, GR_CY_1:21; hence ex a being Element of G st ord a = p by A2, GR_CY_1:19; ::_thesis: verum end; theorem :: GROUP_8:2 for G being Group for H being Subgroup of G for a1, a2 being Element of H for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds a1 * a2 = b1 * b2 proof let G be Group; ::_thesis: for H being Subgroup of G for a1, a2 being Element of H for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds a1 * a2 = b1 * b2 let H be Subgroup of G; ::_thesis: for a1, a2 being Element of H for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds a1 * a2 = b1 * b2 let a1, a2 be Element of H; ::_thesis: for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds a1 * a2 = b1 * b2 A1: the carrier of H c= the carrier of G by GROUP_2:def_5; let b1, b2 be Element of G; ::_thesis: ( a1 = b1 & a2 = b2 implies a1 * a2 = b1 * b2 ) assume that A2: a1 = b1 and A3: a2 = b2 ; ::_thesis: a1 * a2 = b1 * b2 dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1; then A4: the multF of G is ManySortedSet of [: the carrier of G, the carrier of G:] by PARTFUN1:def_2; the multF of H = the multF of G || the carrier of H by GROUP_2:def_5; hence a1 * a2 = b1 * b2 by A1, A2, A3, A4, ALTCAT_1:5; ::_thesis: verum end; theorem :: GROUP_8:3 for G being Group for H being Subgroup of G for a being Element of H for b being Element of G st a = b holds for n being Element of NAT holds a |^ n = b |^ n by GROUP_4:1; theorem :: GROUP_8:4 for G being Group for H being Subgroup of G for a being Element of H for b being Element of G st a = b holds for i being Integer holds a |^ i = b |^ i by GROUP_4:2; theorem :: GROUP_8:5 for G being Group for H being Subgroup of G for a being Element of H for b being Element of G st a = b & G is finite holds ord a = ord b proof let G be Group; ::_thesis: for H being Subgroup of G for a being Element of H for b being Element of G st a = b & G is finite holds ord a = ord b let H be Subgroup of G; ::_thesis: for a being Element of H for b being Element of G st a = b & G is finite holds ord a = ord b let a be Element of H; ::_thesis: for b being Element of G st a = b & G is finite holds ord a = ord b let b be Element of G; ::_thesis: ( a = b & G is finite implies ord a = ord b ) assume that A1: a = b and A2: G is finite ; ::_thesis: ord a = ord b A3: not a is being_of_order_0 by A2, GR_CY_1:6; A4: not b is being_of_order_0 by A2, GR_CY_1:6; A5: a |^ (ord a) = 1_ H by A3, GROUP_1:def_11; A6: b |^ (ord b) = 1_ G by A4, GROUP_1:def_11; a |^ (ord a) = b |^ (ord a) by A1, GROUP_4:1; then A7: ord b divides ord a by A5, A6, GROUP_1:44, GROUP_2:44; a |^ (ord b) = 1_ G by A1, A6, GROUP_4:1; then a |^ (ord b) = 1_ H by GROUP_2:44; then ord a divides ord b by GROUP_1:44; hence ord a = ord b by A7, NAT_D:5; ::_thesis: verum end; theorem :: GROUP_8:6 for G being Group for H being Subgroup of G for h being Element of G st h in H holds H * h c= the carrier of H proof let G be Group; ::_thesis: for H being Subgroup of G for h being Element of G st h in H holds H * h c= the carrier of H let H be Subgroup of G; ::_thesis: for h being Element of G st h in H holds H * h c= the carrier of H let h be Element of G; ::_thesis: ( h in H implies H * h c= the carrier of H ) assume A1: h in H ; ::_thesis: H * h c= the carrier of H for a being set st a in H * h holds a in the carrier of H proof let a be set ; ::_thesis: ( a in H * h implies a in the carrier of H ) assume a in H * h ; ::_thesis: a in the carrier of H then consider g being Element of G such that A2: a = g * h and A3: g in H by GROUP_2:104; g * h in H by A1, A3, GROUP_2:50; hence a in the carrier of H by A2, STRUCT_0:def_5; ::_thesis: verum end; hence H * h c= the carrier of H by TARSKI:def_3; ::_thesis: verum end; theorem Th7: :: GROUP_8:7 for G being Group for a being Element of G st a <> 1_ G holds gr {a} <> (1). G proof let G be Group; ::_thesis: for a being Element of G st a <> 1_ G holds gr {a} <> (1). G let a be Element of G; ::_thesis: ( a <> 1_ G implies gr {a} <> (1). G ) assume A1: a <> 1_ G ; ::_thesis: gr {a} <> (1). G assume A2: gr {a} = (1). G ; ::_thesis: contradiction A3: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7; A4: {a} c= the carrier of (gr {a}) by GROUP_4:def_4; for xx being set st xx = a holds xx = 1_ G proof let xx be set ; ::_thesis: ( xx = a implies xx = 1_ G ) assume xx = a ; ::_thesis: xx = 1_ G then xx in {a} by TARSKI:def_1; hence xx = 1_ G by A2, A3, A4, TARSKI:def_1; ::_thesis: verum end; hence contradiction by A1; ::_thesis: verum end; theorem :: GROUP_8:8 for G being Group for m being Integer holds (1_ G) |^ m = 1_ G by GROUP_1:31; theorem Th9: :: GROUP_8:9 for G being strict Group for a being Element of G for m being Integer holds a |^ (m * (ord a)) = 1_ G proof let G be strict Group; ::_thesis: for a being Element of G for m being Integer holds a |^ (m * (ord a)) = 1_ G let a be Element of G; ::_thesis: for m being Integer holds a |^ (m * (ord a)) = 1_ G let m be Integer; ::_thesis: a |^ (m * (ord a)) = 1_ G percases ( a is being_of_order_0 or not a is being_of_order_0 ) ; suppose a is being_of_order_0 ; ::_thesis: a |^ (m * (ord a)) = 1_ G then ord a = 0 by GROUP_1:def_11; hence a |^ (m * (ord a)) = 1_ G by GROUP_1:25; ::_thesis: verum end; suppose not a is being_of_order_0 ; ::_thesis: a |^ (m * (ord a)) = 1_ G then A1: a |^ (ord a) = 1_ G by GROUP_1:def_11; (1_ G) |^ m = 1_ G by GROUP_1:31; hence a |^ (m * (ord a)) = 1_ G by A1, GROUP_1:35; ::_thesis: verum end; end; end; theorem Th10: :: GROUP_8:10 for G being strict Group for a being Element of G st not a is being_of_order_0 holds for m being Integer holds a |^ m = a |^ (m mod (ord a)) proof let G be strict Group; ::_thesis: for a being Element of G st not a is being_of_order_0 holds for m being Integer holds a |^ m = a |^ (m mod (ord a)) let a be Element of G; ::_thesis: ( not a is being_of_order_0 implies for m being Integer holds a |^ m = a |^ (m mod (ord a)) ) assume A1: not a is being_of_order_0 ; ::_thesis: for m being Integer holds a |^ m = a |^ (m mod (ord a)) let m be Integer; ::_thesis: a |^ m = a |^ (m mod (ord a)) ord a <> 0 by A1, GROUP_1:def_11; then m mod (ord a) = m - ((m div (ord a)) * (ord a)) by INT_1:def_10; then a |^ (m mod (ord a)) = a |^ (m + (- ((1 * (m div (ord a))) * (ord a)))) .= (a |^ m) * (a |^ ((- (m div (ord a))) * (ord a))) by GROUP_1:33 .= (a |^ m) * (1_ G) by Th9 .= a |^ m by GROUP_1:def_4 ; hence a |^ m = a |^ (m mod (ord a)) ; ::_thesis: verum end; theorem Th11: :: GROUP_8:11 for G being strict Group for b being Element of G st not b is being_of_order_0 holds gr {b} is finite proof let G be strict Group; ::_thesis: for b being Element of G st not b is being_of_order_0 holds gr {b} is finite let b be Element of G; ::_thesis: ( not b is being_of_order_0 implies gr {b} is finite ) assume A1: not b is being_of_order_0 ; ::_thesis: gr {b} is finite then A2: ord b <> 0 by GROUP_1:def_11; deffunc H1( Nat) -> Element of the carrier of G = b |^ \$1; consider f being FinSequence such that A3: ( len f = ord b & ( for i being Nat st i in dom f holds f . i = H1(i) ) ) from FINSEQ_1:sch_2(); A4: dom f = Seg (ord b) by A3, FINSEQ_1:def_3; the carrier of (gr {b}) c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (gr {b}) or x in rng f ) assume x in the carrier of (gr {b}) ; ::_thesis: x in rng f then A5: x in gr {b} by STRUCT_0:def_5; then x in G by GROUP_2:40; then reconsider a = x as Element of G by STRUCT_0:def_5; consider m being Integer such that A6: a = b |^ m by A5, GR_CY_1:5; set k = m mod (ord b); reconsider k = m mod (ord b) as Element of NAT by INT_1:3, NEWTON:64; A7: a = b |^ k by A1, A6, Th10; percases ( k = 0 or k <> 0 ) ; supposeA8: k = 0 ; ::_thesis: x in rng f ord b >= 0 + 1 by A2, NAT_1:13; then A9: ord b in Seg (ord b) by FINSEQ_1:1; a = 1_ G by A7, A8, GROUP_1:25 .= b |^ (ord b) by A1, GROUP_1:def_11 .= f . (ord b) by A3, A4, A9 ; hence x in rng f by A4, A9, FUNCT_1:def_3; ::_thesis: verum end; supposeA10: k <> 0 ; ::_thesis: x in rng f A11: k < ord b by A2, NEWTON:65; k >= 0 + 1 by A10, NAT_1:13; then A12: k in Seg (ord b) by A11, FINSEQ_1:1; then a = f . k by A3, A4, A7; hence x in rng f by A4, A12, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence the carrier of (gr {b}) is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum end; theorem Th12: :: GROUP_8:12 for G being strict Group for b being Element of G st b is being_of_order_0 holds b " is being_of_order_0 proof let G be strict Group; ::_thesis: for b being Element of G st b is being_of_order_0 holds b " is being_of_order_0 let b be Element of G; ::_thesis: ( b is being_of_order_0 implies b " is being_of_order_0 ) assume A1: b is being_of_order_0 ; ::_thesis: b " is being_of_order_0 for n being Nat st (b ") |^ n = 1_ G holds n = 0 proof let n be Nat; ::_thesis: ( (b ") |^ n = 1_ G implies n = 0 ) assume (b ") |^ n = 1_ G ; ::_thesis: n = 0 then (b |^ n) " = 1_ G by GROUP_1:37; then (b |^ n) " = (1_ G) " by GROUP_1:8; then b |^ n = 1_ G by GROUP_1:9; hence n = 0 by A1, GROUP_1:def_10; ::_thesis: verum end; hence b " is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum end; theorem Th13: :: GROUP_8:13 for G being strict Group for b being Element of G holds ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds n = 0 ) proof let G be strict Group; ::_thesis: for b being Element of G holds ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds n = 0 ) let b be Element of G; ::_thesis: ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds n = 0 ) thus ( b is being_of_order_0 implies for n being Integer st b |^ n = 1_ G holds n = 0 ) ::_thesis: ( ( for n being Integer st b |^ n = 1_ G holds n = 0 ) implies b is being_of_order_0 ) proof assume A1: b is being_of_order_0 ; ::_thesis: for n being Integer st b |^ n = 1_ G holds n = 0 A2: for m being Element of NAT st b |^ (- m) = 1_ G holds m = 0 proof let m be Element of NAT ; ::_thesis: ( b |^ (- m) = 1_ G implies m = 0 ) assume A3: b |^ (- m) = 1_ G ; ::_thesis: m = 0 b |^ (- m) = (b |^ m) " by GROUP_1:36; then A4: (b ") |^ m = 1_ G by A3, GROUP_1:37; b " is being_of_order_0 by A1, Th12; hence m = 0 by A4, GROUP_1:def_10; ::_thesis: verum end; for n being Integer st b |^ n = 1_ G holds n = 0 proof let n be Integer; ::_thesis: ( b |^ n = 1_ G implies n = 0 ) assume A5: b |^ n = 1_ G ; ::_thesis: n = 0 consider k being Element of NAT such that A6: ( n = k or n = - k ) by INT_1:2; percases ( n = k or n = - k ) by A6; suppose n = k ; ::_thesis: n = 0 hence n = 0 by A1, A5, GROUP_1:def_10; ::_thesis: verum end; supposeA7: n = - k ; ::_thesis: n = 0 then k = 0 by A2, A5; hence n = 0 by A7; ::_thesis: verum end; end; end; hence for n being Integer st b |^ n = 1_ G holds n = 0 ; ::_thesis: verum end; assume for n being Integer st b |^ n = 1_ G holds n = 0 ; ::_thesis: b is being_of_order_0 then for n being Nat st b |^ n = 1_ G holds n = 0 ; hence b is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum end; theorem :: GROUP_8:14 for G being strict Group st ex a being Element of G st a <> 1_ G holds ( ( for H being strict Subgroup of G holds ( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) ) proof let G be strict Group; ::_thesis: ( ex a being Element of G st a <> 1_ G implies ( ( for H being strict Subgroup of G holds ( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) ) ) assume A1: ex a being Element of G st a <> 1_ G ; ::_thesis: ( ( for H being strict Subgroup of G holds ( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) ) thus ( ( for H being strict Subgroup of G holds ( H = G or H = (1). G ) ) implies ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) ) ::_thesis: ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) implies for H being strict Subgroup of G holds ( H = G or H = (1). G ) ) proof assume A2: for H being strict Subgroup of G holds ( H = G or H = (1). G ) ; ::_thesis: ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) consider b being Element of G such that A3: b <> 1_ G by A1; A4: gr {b} = G by A2, A3, Th7; A5: not b is being_of_order_0 proof assume A6: b is being_of_order_0 ; ::_thesis: contradiction then A7: b |^ 2 <> 1_ G by GROUP_1:def_10; not b in gr {(b |^ 2)} proof assume b in gr {(b |^ 2)} ; ::_thesis: contradiction then consider j1 being Integer such that A8: b = (b |^ 2) |^ j1 by GR_CY_1:5; b = b |^ (2 * j1) by A8, GROUP_1:35; then (b ") * (b |^ (2 * j1)) = 1_ G by GROUP_1:def_5; then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:32; then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:33; then (- 1) + (2 * j1) = 0 by A6, Th13; hence contradiction by INT_1:9; ::_thesis: verum end; then gr {(b |^ 2)} <> G by A4, GR_CY_2:2; hence contradiction by A2, A7, Th7; ::_thesis: verum end; then consider n being Element of NAT such that A9: n = ord b and not b is being_of_order_0 ; A10: G is finite by A4, A5, Th11; then A11: card G = n by A4, A9, GR_CY_1:7; n is prime proof assume A12: not n is prime ; ::_thesis: contradiction ex u, v being Element of NAT st ( u > 1 & v > 1 & n = u * v ) proof A13: ( not n > 1 or ex m being Nat st ( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def_4; n >= 1 by A10, A11, GROUP_1:45; then n > 1 by A3, A9, GROUP_1:43, XXREAL_0:1; then consider m being Nat such that A14: m <> 1 and A15: m <> n and A16: m divides n by A13; reconsider m = m as Element of NAT by ORDINAL1:def_12; consider o being Nat such that A17: n = m * o by A16, NAT_D:def_3; reconsider o = o as Element of NAT by ORDINAL1:def_12; take u = m; ::_thesis: ex v being Element of NAT st ( u > 1 & v > 1 & n = u * v ) take v = o; ::_thesis: ( u > 1 & v > 1 & n = u * v ) u <> 0 proof assume u = 0 ; ::_thesis: contradiction then n = 0 * (n div 0) by A16, NAT_D:3; hence contradiction by A10, A11; ::_thesis: verum end; then A18: 0 + 1 <= u by INT_1:7; 0 < v by A10, A11, A17; then A19: 0 + 1 <= v by INT_1:7; v <> 1 by A15, A17; hence ( u > 1 & v > 1 & n = u * v ) by A14, A17, A18, A19, XXREAL_0:1; ::_thesis: verum end; then consider u, v being Element of NAT such that A20: u > 1 and A21: v > 1 and A22: n = u * v ; ord (b |^ v) = u by A4, A10, A11, A22, GR_CY_2:8; then A23: card (gr {(b |^ v)}) = u by A10, GR_CY_1:7; A24: u <> n by A20, A21, A22, XCMPLX_1:7; gr {(b |^ v)} <> (1). G by A20, A23, GROUP_2:69; hence contradiction by A2, A11, A23, A24; ::_thesis: verum end; hence ( G is cyclic & G is finite & ex p being Element of NAT st ( card G = p & p is prime ) ) by A4, A5, A11, Th11, GR_CY_2:4; ::_thesis: verum end; assume that G is cyclic and A25: G is finite and A26: ex p being Element of NAT st ( card G = p & p is prime ) ; ::_thesis: for H being strict Subgroup of G holds ( H = G or H = (1). G ) let H be strict Subgroup of G; ::_thesis: ( H = G or H = (1). G ) reconsider G = G as finite Group by A25; reconsider H = H as Subgroup of G ; card G = (card H) * (index H) by GROUP_2:147; then A27: card H divides card G by NAT_D:def_3; percases ( card H = card G or card H = 1 ) by A26, A27, INT_2:def_4; suppose card H = card G ; ::_thesis: ( H = G or H = (1). G ) hence ( H = G or H = (1). G ) by GROUP_2:73; ::_thesis: verum end; suppose card H = 1 ; ::_thesis: ( H = G or H = (1). G ) hence ( H = G or H = (1). G ) by GROUP_2:70; ::_thesis: verum end; end; end; theorem Th15: :: GROUP_8:15 for G being Group for x, y, z being Element of G for A being Subset of G holds ( z in (x * A) * y iff ex a being Element of G st ( z = (x * a) * y & a in A ) ) proof let G be Group; ::_thesis: for x, y, z being Element of G for A being Subset of G holds ( z in (x * A) * y iff ex a being Element of G st ( z = (x * a) * y & a in A ) ) let x, y, z be Element of G; ::_thesis: for A being Subset of G holds ( z in (x * A) * y iff ex a being Element of G st ( z = (x * a) * y & a in A ) ) let A be Subset of G; ::_thesis: ( z in (x * A) * y iff ex a being Element of G st ( z = (x * a) * y & a in A ) ) thus ( z in (x * A) * y implies ex a being Element of G st ( z = (x * a) * y & a in A ) ) ::_thesis: ( ex a being Element of G st ( z = (x * a) * y & a in A ) implies z in (x * A) * y ) proof assume z in (x * A) * y ; ::_thesis: ex a being Element of G st ( z = (x * a) * y & a in A ) then consider b being Element of G such that A1: z = b * y and A2: b in x * A by GROUP_2:28; consider u being Element of G such that A3: b = x * u and A4: u in A by A2, GROUP_2:27; take u ; ::_thesis: ( z = (x * u) * y & u in A ) thus ( z = (x * u) * y & u in A ) by A1, A3, A4; ::_thesis: verum end; given a being Element of G such that A5: z = (x * a) * y and A6: a in A ; ::_thesis: z in (x * A) * y ex h being Element of G st ( z = h * y & h in x * A ) proof take x * a ; ::_thesis: ( z = (x * a) * y & x * a in x * A ) thus ( z = (x * a) * y & x * a in x * A ) by A5, A6, GROUP_2:27; ::_thesis: verum end; hence z in (x * A) * y by GROUP_2:28; ::_thesis: verum end; theorem :: GROUP_8:16 for G being Group for A being non empty Subset of G for x being Element of G holds card A = card (((x ") * A) * x) proof let G be Group; ::_thesis: for A being non empty Subset of G for x being Element of G holds card A = card (((x ") * A) * x) let A be non empty Subset of G; ::_thesis: for x being Element of G holds card A = card (((x ") * A) * x) let x be Element of G; ::_thesis: card A = card (((x ") * A) * x) set B = ((x ") * A) * x; ( not A is empty & not ((x ") * A) * x is empty ) proof set a = the Element of A; ((x ") * the Element of A) * x in ((x ") * A) * x by Th15; hence ( not A is empty & not ((x ") * A) * x is empty ) ; ::_thesis: verum end; then reconsider B = ((x ") * A) * x as non empty Subset of G ; deffunc H1( Element of G) -> Element of the carrier of G = ((x ") * \$1) * x; consider f being Function of A, the carrier of G such that A1: for a being Element of A holds f . a = H1(a) from FUNCT_2:sch_4(); A2: dom f = A by FUNCT_2:def_1; A3: rng f c= B proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng f or s in B ) assume s in rng f ; ::_thesis: s in B then consider a being set such that A4: a in A and A5: s = f . a by A2, FUNCT_1:def_3; reconsider a = a as Element of A by A4; s = H1(a) by A1, A5; hence s in B by Th15; ::_thesis: verum end; A6: B c= rng f proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in B or s in rng f ) assume s in B ; ::_thesis: s in rng f then consider a being Element of G such that A7: s = ((x ") * a) * x and A8: a in A by Th15; ex x being Element of G st ( x in dom f & s = f . x ) proof take a ; ::_thesis: ( a in dom f & s = f . a ) thus ( a in dom f & s = f . a ) by A1, A7, A8, FUNCT_2:def_1; ::_thesis: verum end; hence s in rng f by FUNCT_1:def_3; ::_thesis: verum end; reconsider f = f as Function of A,B by A2, A3, FUNCT_2:2; deffunc H2( Element of G) -> Element of the carrier of G = (x * \$1) * (x "); consider g being Function of B, the carrier of G such that A9: for b being Element of B holds g . b = H2(b) from FUNCT_2:sch_4(); A10: dom g = B by FUNCT_2:def_1; rng g c= A proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng g or s in A ) assume s in rng g ; ::_thesis: s in A then consider a being set such that A11: a in B and A12: s = g . a by A10, FUNCT_1:def_3; reconsider a = a as Element of B by A11; A13: s = H2(a) by A9, A12; consider c being Element of G such that A14: a = ((x ") * c) * x and A15: c in A by Th15; s = ((x * ((x ") * c)) * x) * (x ") by A13, A14, GROUP_1:def_3 .= (((x * (x ")) * c) * x) * (x ") by GROUP_1:def_3 .= ((x * (x ")) * c) * (x * (x ")) by GROUP_1:def_3 .= ((1_ G) * c) * (x * (x ")) by GROUP_1:def_5 .= ((1_ G) * c) * (1_ G) by GROUP_1:def_5 .= (1_ G) * c by GROUP_1:def_4 .= c by GROUP_1:def_4 ; hence s in A by A15; ::_thesis: verum end; then reconsider g = g as Function of B,A by A10, FUNCT_2:2; A16: for a, b being Element of A st f . a = f . b holds a = b proof let a, b be Element of A; ::_thesis: ( f . a = f . b implies a = b ) assume A17: f . a = f . b ; ::_thesis: a = b A18: ((x ") * a) * x in B by Th15; A19: ((x ") * b) * x in B by Th15; A20: g . (f . a) = g . (((x ") * a) * x) by A1 .= (x * (((x ") * a) * x)) * (x ") by A9, A18 .= ((x * ((x ") * a)) * x) * (x ") by GROUP_1:def_3 .= (((x * (x ")) * a) * x) * (x ") by GROUP_1:def_3 .= ((x * (x ")) * a) * (x * (x ")) by GROUP_1:def_3 .= ((1_ G) * a) * (x * (x ")) by GROUP_1:def_5 .= a * (x * (x ")) by GROUP_1:def_4 .= a * (1_ G) by GROUP_1:def_5 .= a by GROUP_1:def_4 ; g . (f . b) = g . (((x ") * b) * x) by A1 .= (x * (((x ") * b) * x)) * (x ") by A9, A19 .= ((x * ((x ") * b)) * x) * (x ") by GROUP_1:def_3 .= (((x * (x ")) * b) * x) * (x ") by GROUP_1:def_3 .= ((x * (x ")) * b) * (x * (x ")) by GROUP_1:def_3 .= ((1_ G) * b) * (x * (x ")) by GROUP_1:def_5 .= b * (x * (x ")) by GROUP_1:def_4 .= b * (1_ G) by GROUP_1:def_5 .= b by GROUP_1:def_4 ; hence a = b by A17, A20; ::_thesis: verum end; A,B are_equipotent proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = A & rng f = B ) thus ( f is one-to-one & dom f = A & rng f = B ) by A3, A6, A16, FUNCT_2:def_1, GROUP_6:1, XBOOLE_0:def_10; ::_thesis: verum end; hence card A = card (((x ") * A) * x) by CARD_1:5; ::_thesis: verum end; definition let G be strict Group; let H, K be strict Subgroup of G; func Double_Cosets (H,K) -> Subset-Family of G means :: GROUP_8:def 1 for A being Subset of G holds ( A in it iff ex a being Element of G st A = (H * a) * K ); existence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = (H * a) * K ) proof defpred S1[ set ] means ex a being Element of G st \$1 = (H * a) * K; ex F being Subset-Family of G st for A being Subset of G holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of G st for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = (H * a) * K ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of G st ( for A being Subset of G holds ( A in b1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds ( A in b2 iff ex a being Element of G st A = (H * a) * K ) ) holds b1 = b2 proof let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds ( A in F1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds ( A in F2 iff ex a being Element of G st A = (H * a) * K ) ) implies F1 = F2 ) defpred S1[ set ] means ex a being Element of G st \$1 = (H * a) * K; assume A1: for A being Subset of G holds ( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st ( ( A in F2 implies ex a being Element of G st A = (H * a) * K ) implies ( ex a being Element of G st A = (H * a) * K & not A in F2 ) ) or F1 = F2 ) assume A2: for A being Subset of G holds ( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2 thus F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum end; end; :: deftheorem defines Double_Cosets GROUP_8:def_1_:_ for G being strict Group for H, K being strict Subgroup of G for b4 being Subset-Family of G holds ( b4 = Double_Cosets (H,K) iff for A being Subset of G holds ( A in b4 iff ex a being Element of G st A = (H * a) * K ) ); theorem Th17: :: GROUP_8:17 for G being strict Group for z, x being Element of G for H, K being strict Subgroup of G holds ( z in (H * x) * K iff ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) ) proof let G be strict Group; ::_thesis: for z, x being Element of G for H, K being strict Subgroup of G holds ( z in (H * x) * K iff ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) ) let z, x be Element of G; ::_thesis: for H, K being strict Subgroup of G holds ( z in (H * x) * K iff ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) ) let H, K be strict Subgroup of G; ::_thesis: ( z in (H * x) * K iff ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) ) thus ( z in (H * x) * K implies ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) ) ::_thesis: ( ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) implies z in (H * x) * K ) proof assume z in (H * x) * K ; ::_thesis: ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) then consider g1, g2 being Element of G such that A1: z = g1 * g2 and A2: g1 in H * x and A3: g2 in K by GROUP_2:94; ex h1 being Element of G st ( g1 = h1 * x & h1 in H ) by A2, GROUP_2:104; hence ex g, h being Element of G st ( z = (g * x) * h & g in H & h in K ) by A1, A3; ::_thesis: verum end; given g, h being Element of G such that A4: z = (g * x) * h and A5: g in H and A6: h in K ; ::_thesis: z in (H * x) * K ex g1, g2 being Element of G st ( z = g1 * g2 & g1 in H * x & g2 in K ) proof set g1 = g * x; g * x in H * x by A5, GROUP_2:104; hence ex g1, g2 being Element of G st ( z = g1 * g2 & g1 in H * x & g2 in K ) by A4, A6; ::_thesis: verum end; hence z in (H * x) * K by GROUP_2:94; ::_thesis: verum end; theorem :: GROUP_8:18 for G being strict Group for x, y being Element of G for H, K being strict Subgroup of G holds ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) proof let G be strict Group; ::_thesis: for x, y being Element of G for H, K being strict Subgroup of G holds ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) let x, y be Element of G; ::_thesis: for H, K being strict Subgroup of G holds ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) let H, K be strict Subgroup of G; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) percases ( for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st ( z in (H * x) * K & z in (H * y) * K ) ) ; suppose for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) hence ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) ; ::_thesis: verum end; suppose ex z being Element of G st ( z in (H * x) * K & z in (H * y) * K ) ; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) then consider z being Element of G such that A1: z in (H * x) * K and A2: z in (H * y) * K ; consider h1, k1 being Element of G such that A3: z = (h1 * x) * k1 and A4: h1 in H and A5: k1 in K by A1, Th17; consider h2, k2 being Element of G such that A6: z = (h2 * y) * k2 and A7: h2 in H and A8: k2 in K by A2, Th17; for a being set st a in (H * x) * K holds a in (H * y) * K proof let a be set ; ::_thesis: ( a in (H * x) * K implies a in (H * y) * K ) assume a in (H * x) * K ; ::_thesis: a in (H * y) * K then consider h, k being Element of G such that A9: a = (h * x) * k and A10: h in H and A11: k in K by Th17; ex c, d being Element of G st ( a = (c * y) * d & c in H & d in K ) proof h = h * (1_ G) by GROUP_1:def_4; then A12: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def_4; 1_ G = (h1 ") * h1 by GROUP_1:def_5; then A13: (h * x) * k = (((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k by A12, GROUP_1:def_5 .= ((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k by GROUP_1:def_3 .= (((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k by GROUP_1:def_3 .= ((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k by GROUP_1:def_3 .= (((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k by A3, A6, GROUP_1:def_3 .= ((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k by GROUP_1:def_3 .= (((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k by GROUP_1:def_3 .= ((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k by GROUP_1:def_3 .= (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) by GROUP_1:def_3 ; take (h * (h1 ")) * h2 ; ::_thesis: ex d being Element of G st ( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K ) take (k2 * (k1 ")) * k ; ::_thesis: ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) h1 " in H by A4, GROUP_2:51; then A14: h * (h1 ") in H by A10, GROUP_2:50; k1 " in K by A5, GROUP_2:51; then k2 * (k1 ") in K by A8, GROUP_2:50; hence ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) by A7, A9, A11, A13, A14, GROUP_2:50; ::_thesis: verum end; hence a in (H * y) * K by Th17; ::_thesis: verum end; then A15: (H * x) * K c= (H * y) * K by TARSKI:def_3; for a being set st a in (H * y) * K holds a in (H * x) * K proof let a be set ; ::_thesis: ( a in (H * y) * K implies a in (H * x) * K ) assume a in (H * y) * K ; ::_thesis: a in (H * x) * K then consider h, k being Element of G such that A16: a = (h * y) * k and A17: h in H and A18: k in K by Th17; ex c, d being Element of G st ( a = (c * x) * d & c in H & d in K ) proof h = h * (1_ G) by GROUP_1:def_4; then A19: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def_4; 1_ G = (h2 ") * h2 by GROUP_1:def_5; then A20: (h * y) * k = (((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k by A19, GROUP_1:def_5 .= ((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k by GROUP_1:def_3 .= (((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k by GROUP_1:def_3 .= ((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k by GROUP_1:def_3 .= (((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k by A3, A6, GROUP_1:def_3 .= ((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k by GROUP_1:def_3 .= (((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k by GROUP_1:def_3 .= ((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k by GROUP_1:def_3 .= (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) by GROUP_1:def_3 ; take (h * (h2 ")) * h1 ; ::_thesis: ex d being Element of G st ( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K ) take (k1 * (k2 ")) * k ; ::_thesis: ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) h2 " in H by A7, GROUP_2:51; then A21: h * (h2 ") in H by A17, GROUP_2:50; k2 " in K by A8, GROUP_2:51; then k1 * (k2 ") in K by A5, GROUP_2:50; hence ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) by A4, A16, A18, A20, A21, GROUP_2:50; ::_thesis: verum end; hence a in (H * x) * K by Th17; ::_thesis: verum end; then (H * y) * K c= (H * x) * K by TARSKI:def_3; hence ( (H * x) * K = (H * y) * K or for z being Element of G holds ( not z in (H * x) * K or not z in (H * y) * K ) ) by A15, XBOOLE_0:def_10; ::_thesis: verum end; end; end; registration let G be Group; let A be Subgroup of G; cluster Left_Cosets A -> non empty ; coherence not Left_Cosets A is empty by GROUP_2:135; end; notation let G be Group; let H be Subgroup of G; synonym index (G,H) for index H; end; theorem Th19: :: GROUP_8:19 for G being Group for A, B being Subgroup of G for D being Subgroup of A st D = A /\ B & G is finite holds index (G,B) >= index (A,D) proof let G be Group; ::_thesis: for A, B being Subgroup of G for D being Subgroup of A st D = A /\ B & G is finite holds index (G,B) >= index (A,D) let A, B be Subgroup of G; ::_thesis: for D being Subgroup of A st D = A /\ B & G is finite holds index (G,B) >= index (A,D) let D be Subgroup of A; ::_thesis: ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) ) assume that A1: D = A /\ B and A2: G is finite ; ::_thesis: index (G,B) >= index (A,D) reconsider LCB = Left_Cosets B as non empty finite set by A2; reconsider LCD = Left_Cosets D as non empty finite set by A2; A3: now__::_thesis:_for_x,_y_being_Element_of_G for_x9,_y9_being_Element_of_A_st_x9_=_x_&_y9_=_y_holds_ (_x_*_B_=_y_*_B_iff_x9_*_D_=_y9_*_D_) let x, y be Element of G; ::_thesis: for x9, y9 being Element of A st x9 = x & y9 = y holds ( x * B = y * B iff x9 * D = y9 * D ) let x9, y9 be Element of A; ::_thesis: ( x9 = x & y9 = y implies ( x * B = y * B iff x9 * D = y9 * D ) ) assume that A4: x9 = x and A5: y9 = y ; ::_thesis: ( x * B = y * B iff x9 * D = y9 * D ) A6: y9 " = y " by A5, GROUP_2:48; A7: (y9 ") * x9 in A by STRUCT_0:def_5; ( x * B = y * B iff (y ") * x in B ) by GROUP_2:114; then ( x * B = y * B iff (y9 ") * x9 in B ) by A4, A6, GROUP_2:43; then ( x * B = y * B iff (y9 ") * x9 in D ) by A1, A7, GROUP_2:82; hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; ::_thesis: verum end; defpred S1[ set , set ] means ex a being Element of G ex a9 being Element of A st ( a = a9 & \$2 = a * B & \$1 = a9 * D ); A8: for x being Element of LCD ex y being Element of LCB st S1[x,y] proof let x be Element of LCD; ::_thesis: ex y being Element of LCB st S1[x,y] x in LCD ; then consider a9 being Element of A such that A9: x = a9 * D by GROUP_2:def_15; reconsider a = a9 as Element of G by GROUP_2:42; reconsider y = a * B as Element of LCB by GROUP_2:def_15; take y ; ::_thesis: S1[x,y] take a ; ::_thesis: ex a9 being Element of A st ( a = a9 & y = a * B & x = a9 * D ) take a9 ; ::_thesis: ( a = a9 & y = a * B & x = a9 * D ) thus ( a = a9 & y = a * B & x = a9 * D ) by A9; ::_thesis: verum end; consider F being Function of LCD,LCB such that A10: for a being Element of LCD holds S1[a,F . a] from FUNCT_2:sch_3(A8); A11: dom F = LCD by FUNCT_2:def_1; A12: rng F c= LCB by RELAT_1:def_19; A13: index D = card LCD by GROUP_2:def_18; A14: index B = card LCB by GROUP_2:def_18; F is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 ) assume that A15: x1 in dom F and A16: x2 in dom F ; ::_thesis: ( not F . x1 = F . x2 or x1 = x2 ) reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def_1; A17: ex a being Element of G ex a9 being Element of A st ( a = a9 & F . z1 = a * B & z1 = a9 * D ) by A10; ex b being Element of G ex b9 being Element of A st ( b = b9 & F . z2 = b * B & z2 = b9 * D ) by A10; hence ( not F . x1 = F . x2 or x1 = x2 ) by A3, A17; ::_thesis: verum end; then index D c= index B by A11, A12, A13, A14, CARD_1:10; hence index (G,B) >= index (A,D) by NAT_1:39; ::_thesis: verum end; theorem Th20: :: GROUP_8:20 for G being finite Group for H being Subgroup of G holds index (G,H) > 0 proof let G be finite Group; ::_thesis: for H being Subgroup of G holds index (G,H) > 0 let H be Subgroup of G; ::_thesis: index (G,H) > 0 card G = (card H) * (index H) by GROUP_2:147; hence index (G,H) > 0 ; ::_thesis: verum end; theorem :: GROUP_8:21 for G being Group st G is finite holds for C being Subgroup of G for A, B being Subgroup of C for D being Subgroup of A st D = A /\ B holds for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) proof let G be Group; ::_thesis: ( G is finite implies for C being Subgroup of G for A, B being Subgroup of C for D being Subgroup of A st D = A /\ B holds for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) ) assume A1: G is finite ; ::_thesis: for C being Subgroup of G for A, B being Subgroup of C for D being Subgroup of A st D = A /\ B holds for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) let C be Subgroup of G; ::_thesis: for A, B being Subgroup of C for D being Subgroup of A st D = A /\ B holds for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) let A, B be Subgroup of C; ::_thesis: for D being Subgroup of A st D = A /\ B holds for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) let D be Subgroup of A; ::_thesis: ( D = A /\ B implies for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) ) assume A2: D = A /\ B ; ::_thesis: for E being Subgroup of B st E = A /\ B holds for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) let E be Subgroup of B; ::_thesis: ( E = A /\ B implies for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) ) assume A3: E = A /\ B ; ::_thesis: for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) let F be Subgroup of C; ::_thesis: ( F = A /\ B & index (C,A), index (C,B) are_relative_prime implies ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) ) assume A4: F = A /\ B ; ::_thesis: ( not index (C,A), index (C,B) are_relative_prime or ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) ) assume A5: index A, index B are_relative_prime ; ::_thesis: ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) index F = (index E) * (index B) by A1, A3, A4, GROUP_2:149; then A6: (index E) * (index B) = (index D) * (index A) by A1, A2, A4, GROUP_2:149; then index B divides (index A) * (index D) by INT_1:def_3; then A7: index B divides index D by A5, INT_2:25; ex n being Element of NAT st index D = (index B) * n proof consider i being Integer such that A8: index D = (index B) * i by A7, INT_1:def_3; 0 <= i by A1, A8, Th20; then reconsider i = i as Element of NAT by INT_1:3; take i ; ::_thesis: index D = (index B) * i thus index D = (index B) * i by A8; ::_thesis: verum end; then A9: index B divides index D by NAT_D:def_3; A10: index (C,B) >= index (A,D) by A1, A2, Th19; A11: index B = index D proof assume A12: index B <> index D ; ::_thesis: contradiction index D > 0 by A1, Th20; then index B <= index D by A9, NAT_D:7; hence contradiction by A10, A12, XXREAL_0:1; ::_thesis: verum end; index A divides (index B) * (index E) by A6, INT_1:def_3; then A13: index A divides index E by A5, INT_2:25; ex n being Element of NAT st index E = (index A) * n proof consider i being Integer such that A14: index E = (index A) * i by A13, INT_1:def_3; 0 <= i by A1, A14, Th20; then reconsider i = i as Element of NAT by INT_1:3; take i ; ::_thesis: index E = (index A) * i thus index E = (index A) * i by A14; ::_thesis: verum end; then A15: index A divides index E by NAT_D:def_3; A16: index A >= index E by A1, A3, Th19; index A = index E proof assume A17: index A <> index E ; ::_thesis: contradiction index E > 0 by A1, Th20; then index A <= index E by A15, NAT_D:7; hence contradiction by A16, A17, XXREAL_0:1; ::_thesis: verum end; hence ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) by A11; ::_thesis: verum end; theorem Th22: :: GROUP_8:22 for G being Group for H being Subgroup of G for a being Element of G st a in H holds for j being Integer holds a |^ j in H proof let G be Group; ::_thesis: for H being Subgroup of G for a being Element of G st a in H holds for j being Integer holds a |^ j in H let H be Subgroup of G; ::_thesis: for a being Element of G st a in H holds for j being Integer holds a |^ j in H let a be Element of G; ::_thesis: ( a in H implies for j being Integer holds a |^ j in H ) assume A1: a in H ; ::_thesis: for j being Integer holds a |^ j in H let j be Integer; ::_thesis: a |^ j in H consider k being Element of NAT such that A2: ( j = k or j = - k ) by INT_1:2; percases ( j = k or j = - k ) by A2; supposeA3: j = k ; ::_thesis: a |^ j in H defpred S1[ Element of NAT ] means a |^ \$1 in H; a |^ 0 = 1_ G by GROUP_1:25; then A4: S1[ 0 ] by GROUP_2:46; A5: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then (a |^ n) * a in H by A1, GROUP_2:50; hence S1[n + 1] by GROUP_1:34; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A5); hence a |^ j in H by A3; ::_thesis: verum end; supposeA6: j = - k ; ::_thesis: a |^ j in H defpred S1[ Element of NAT ] means a |^ (- \$1) in H; a |^ 0 = 1_ G by GROUP_1:25; then A7: S1[ 0 ] by GROUP_2:46; A8: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A9: S1[n] ; ::_thesis: S1[n + 1] a " in H by A1, GROUP_2:51; then (a |^ (- n)) * (a ") in H by A9, GROUP_2:50; then (a |^ (- n)) * (a |^ (- 1)) in H by GROUP_1:32; then a |^ ((- n) + (- 1)) in H by GROUP_1:33; hence S1[n + 1] ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A8); hence a |^ j in H by A6; ::_thesis: verum end; end; end; theorem Th23: :: GROUP_8:23 for G being strict Group st G <> (1). G holds ex b being Element of G st b <> 1_ G proof let G be strict Group; ::_thesis: ( G <> (1). G implies ex b being Element of G st b <> 1_ G ) assume A1: G <> (1). G ; ::_thesis: ex b being Element of G st b <> 1_ G assume A2: for b being Element of G holds not b <> 1_ G ; ::_thesis: contradiction for x, y being Element of G holds x = y proof let x, y be Element of G; ::_thesis: x = y x = 1_ G by A2; hence x = y by A2; ::_thesis: verum end; then G is trivial by STRUCT_0:def_10; hence contradiction by A1, GROUP_6:12; ::_thesis: verum end; theorem Th24: :: GROUP_8:24 for G being strict Group for a being Element of G st G = gr {a} holds for H being strict Subgroup of G st H <> (1). G holds ex k being Element of NAT st ( 0 < k & a |^ k in H ) proof let G be strict Group; ::_thesis: for a being Element of G st G = gr {a} holds for H being strict Subgroup of G st H <> (1). G holds ex k being Element of NAT st ( 0 < k & a |^ k in H ) let a be Element of G; ::_thesis: ( G = gr {a} implies for H being strict Subgroup of G st H <> (1). G holds ex k being Element of NAT st ( 0 < k & a |^ k in H ) ) assume A1: G = gr {a} ; ::_thesis: for H being strict Subgroup of G st H <> (1). G holds ex k being Element of NAT st ( 0 < k & a |^ k in H ) let H be strict Subgroup of G; ::_thesis: ( H <> (1). G implies ex k being Element of NAT st ( 0 < k & a |^ k in H ) ) assume H <> (1). G ; ::_thesis: ex k being Element of NAT st ( 0 < k & a |^ k in H ) then A2: H <> (1). H by GROUP_2:63; consider c being Element of H such that A3: c <> 1_ H by A2, Th23; A4: c in H by STRUCT_0:def_5; then c in G by GROUP_2:40; then reconsider c = c as Element of G by STRUCT_0:def_5; A5: c in gr {a} by A1, STRUCT_0:def_5; ex j being Integer st ( c = a |^ j & j <> 0 ) proof assume A6: for j being Integer holds ( not c = a |^ j or not j <> 0 ) ; ::_thesis: contradiction consider i being Integer such that A7: c = a |^ i by A5, GR_CY_1:5; A8: a |^ i <> 1_ G by A3, A7, GROUP_2:44; i = 0 by A6, A7; hence contradiction by A8, GROUP_1:25; ::_thesis: verum end; then consider j being Integer such that A9: c = a |^ j and A10: j <> 0 ; consider n being Element of NAT such that A11: ( j = n or j = - n ) by INT_1:2; percases ( j = n or j = - n ) by A11; suppose j = n ; ::_thesis: ex k being Element of NAT st ( 0 < k & a |^ k in H ) hence ex k being Element of NAT st ( 0 < k & a |^ k in H ) by A4, A9, A10; ::_thesis: verum end; supposeA12: j = - n ; ::_thesis: ex k being Element of NAT st ( 0 < k & a |^ k in H ) then A13: 0 < n by A10; (a |^ n) " in H by A4, A9, A12, GROUP_1:36; then ((a |^ n) ") " in H by GROUP_2:51; hence ex k being Element of NAT st ( 0 < k & a |^ k in H ) by A13; ::_thesis: verum end; end; end; theorem :: GROUP_8:25 for G being strict cyclic Group for H being strict Subgroup of G holds H is cyclic Group proof let G be strict cyclic Group; ::_thesis: for H being strict Subgroup of G holds H is cyclic Group let H be strict Subgroup of G; ::_thesis: H is cyclic Group percases ( H = (1). G or H <> (1). G ) ; suppose H = (1). G ; ::_thesis: H is cyclic Group hence H is cyclic Group ; ::_thesis: verum end; supposeA1: H <> (1). G ; ::_thesis: H is cyclic Group consider b being Element of G such that A2: multMagma(# the carrier of G, the multF of G #) = gr {b} by GR_CY_1:def_7; ex m being Nat st ( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds m <= j ) ) proof defpred S1[ Nat] means ( 0 < \$1 & b |^ \$1 in H ); ex k being Element of NAT st S1[k] by A1, A2, Th24; then A3: ex k being Nat st S1[k] ; ex m being Nat st ( S1[m] & ( for j being Nat st S1[j] holds m <= j ) ) from NAT_1:sch_5(A3); hence ex m being Nat st ( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds m <= j ) ) ; ::_thesis: verum end; then consider m being Nat such that A4: 0 < m and A5: b |^ m in H and A6: for j being Nat st 0 < j & b |^ j in H holds m <= j ; set c = b |^ m; reconsider c = b |^ m as Element of H by A5, STRUCT_0:def_5; for a being Element of H ex i being Integer st a = c |^ i proof let a be Element of H; ::_thesis: ex i being Integer st a = c |^ i ex t being Integer st ( b |^ t in H & b |^ t = a ) proof A7: a in G by GROUP_2:41; A8: a in gr {b} by A2, GROUP_2:41; a is Element of G by A7, STRUCT_0:def_5; then consider j1 being Integer such that A9: a = b |^ j1 by A8, GR_CY_1:5; b |^ j1 in H by A9, STRUCT_0:def_5; hence ex t being Integer st ( b |^ t in H & b |^ t = a ) by A9; ::_thesis: verum end; then consider t being Integer such that A10: b |^ t in H and A11: b |^ t = a ; ex r, s being Integer st ( 0 <= s & s < m & t = (m * r) + s ) proof take t div m ; ::_thesis: ex s being Integer st ( 0 <= s & s < m & t = (m * (t div m)) + s ) take t mod m ; ::_thesis: ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) thus ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) by A4, NEWTON:64, NEWTON:65, NEWTON:66; ::_thesis: verum end; then consider r, s being Integer such that A12: 0 <= s and A13: s < m and A14: t = (m * r) + s ; reconsider s = s as Element of NAT by A12, INT_1:3; A15: b |^ t = (b |^ (m * r)) * (b |^ s) by A14, GROUP_1:33 .= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:35 ; A16: (b |^ m) |^ r in H by A5, Th22; b |^ s in H proof set u = b |^ t; set v = (b |^ m) |^ r; A17: (((b |^ m) |^ r) ") * (b |^ t) = ((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) by A15, GROUP_1:def_3 .= (1_ G) * (b |^ s) by GROUP_1:def_5 .= b |^ s by GROUP_1:def_4 ; ((b |^ m) |^ r) " in H by A16, GROUP_2:51; hence b |^ s in H by A10, A17, GROUP_2:50; ::_thesis: verum end; then s = 0 by A6, A13; then b |^ s = 1_ G by GROUP_1:25; then A18: b |^ t = (b |^ m) |^ r by A15, GROUP_1:def_4; (b |^ m) |^ r = c |^ r by GROUP_4:2; hence ex i being Integer st a = c |^ i by A11, A18; ::_thesis: verum end; then H = gr {c} by GR_CY_2:5; hence H is cyclic Group by GR_CY_2:4; ::_thesis: verum end; end; end;