:: Properties of Groups :: by Gijs Geleijnse and Grzegorz Bancerek :: :: Received May 31, 2004 :: Copyright (c) 2004-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, STRUCT_0, GROUP_1, SUBSET_1, GROUP_2, FINSET_1, INT_2, CARD_1, GRAPH_1, RELAT_1, TARSKI, ALGSTR_0, ZFMISC_1, PBOOLE, REALSET1, NEWTON, INT_1, ARYTM_3, GROUP_4, ARYTM_1, NAT_1, FINSEQ_1, FUNCT_1, XXREAL_0, CQC_SIM1, XBOOLE_0, SETFAM_1, GROUP_8; notations XBOOLE_0, CARD_1, TARSKI, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, PBOOLE, INT_1, NAT_1, FINSET_1, GROUP_2, GROUP_4, GR_CY_1, FINSEQ_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, INT_2; constructors WELLORD2, BINOP_1, REAL_1, NAT_D, BINOP_2, REALSET2, GROUP_4, GR_CY_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, FUNCT_1, WELLORD2, STRUCT_0; equalities REALSET1, ALGSTR_0, CARD_1, ORDINAL1; expansions TARSKI, STRUCT_0; theorems GROUP_2, GR_CY_1, GR_CY_2, NAT_1, TARSKI, XBOOLE_0, GROUP_1, CARD_1, GROUP_6, ALTCAT_1, FUNCT_2, GROUP_4, INT_2, XCMPLX_1, INT_1, FINSEQ_1, FUNCT_1, NEWTON, ORDINAL1, NAT_D, XXREAL_0, RELAT_1, PARTFUN1; schemes SUBSET_1, NAT_1, FINSEQ_1, FUNCT_2; begin reserve G for strict Group, a,b,x,y,z for Element of G, H,K for strict Subgroup of G, p for Element of NAT, A for Subset of G; theorem for G being strict finite Group holds p is prime & card G = p implies ex a being Element of G st ord a = p proof let G be strict finite Group; assume that A1: p is prime and A2: card G = p; G is cyclic Group by A1,A2,GR_CY_1:21; hence thesis by A2,GR_CY_1:19; end; theorem for G being Group, H being Subgroup of G, 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, H be Subgroup of G; let a1,a2 be Element of H; A1: the carrier of H c= the carrier of G by GROUP_2:def 5; let b1,b2 be Element of G such that A2: a1 = b1 and A3: a2 = 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 thesis by A1,A2,A3,A4,ALTCAT_1:5; end; theorem for G being Group, H being Subgroup of G, a being Element of H for b being Element of G st a = b for n being Element of NAT holds a|^n = b|^n by GROUP_4:1; theorem for G being Group, H being Subgroup of G, a being Element of H for b being Element of G st a = b for i being Integer holds a|^i = b|^i by GROUP_4:2; theorem for G being Group, H being Subgroup of G, 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, H be Subgroup of G; let a be Element of H; let b be Element of G such that A1: a =b and A2: G is finite; 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 thesis by A7,NAT_D:5; end; theorem for G being Group, H being Subgroup of G, h being Element of G st h in H holds H * h c= the carrier of H proof let G be Group, H be Subgroup of G; let h be Element of G such that A1: h in H; let a be object; assume a in H * 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 thesis by A2; end; theorem Th7: for G being Group for a being Element of G st a <> 1_G holds gr {a} <> (1).G proof let G be Group; let a be Element of G such that A1: a <> 1_G; assume A2: gr {a} = (1).G; 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 holds xx = a implies xx = 1_G proof let xx be set; assume xx = a; then xx in {a} by TARSKI:def 1; hence thesis by A2,A3,A4,TARSKI:def 1; end; hence thesis by A1; end; theorem for G being Group, m being Integer holds (1_G) |^ m = 1_G by GROUP_1:31; theorem Th9: for m being Integer holds a |^ (m * ord a) = 1_G proof let m be Integer; per cases; suppose a is being_of_order_0; then ord a = 0 by GROUP_1:def 11; hence thesis by GROUP_1:25; end; suppose a is not being_of_order_0; then A1: a |^ ord a = 1_G by GROUP_1:def 11; (1_G) |^ m = 1_G by GROUP_1:31; hence thesis by A1,GROUP_1:35; end; end; theorem Th10: for a st a is not being_of_order_0 for m being Integer holds a |^ m = a |^(m mod ord a) proof let a such that A1: a is not being_of_order_0; let m be Integer; 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 thesis; end; theorem Th11: b is not being_of_order_0 implies gr {b} is finite proof assume A1: b is not being_of_order_0; then A2: ord b <> 0 by GROUP_1:def 11; deffunc B(Nat) = 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 = B(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 object; assume x in the carrier of gr {b}; then A5: x in gr {b}; then x in G by GROUP_2:40; then reconsider a = x as Element of G; consider m being Integer such that A6: a = b|^m by A5,GR_CY_1:5; set k = m mod ord b; reconsider k as Element of NAT by INT_1:3,NEWTON:64; A7: a = b|^k by A1,A6,Th10; per cases; suppose A8: k = 0; 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 thesis by A4,A9,FUNCT_1:def 3; end; suppose A10: k <> 0; 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 thesis by A4,A12,FUNCT_1:def 3; end; end; hence the carrier of gr {b} is finite; end; theorem Th12: b is being_of_order_0 implies b" is being_of_order_0 proof assume A1: b is being_of_order_0; for n being Nat st b" |^ n = 1_G holds n = 0 proof let n be Nat; assume b" |^ n = 1_G; 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 thesis by A1,GROUP_1:def 10; end; hence thesis by GROUP_1:def 10; end; theorem Th13: b is being_of_order_0 iff for n being Integer st b |^n = 1_G holds n = 0 proof thus b is being_of_order_0 implies for n being Integer st b |^n = 1_G holds n = 0 proof assume A1: b is being_of_order_0; A2: for m being Nat holds b |^ - m = 1_G implies m = 0 proof let m be Nat; assume A3: b |^ - m = 1_G; 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 thesis by A4,GROUP_1:def 10; end; for n being Integer holds b |^ n = 1_G implies n = 0 proof let n be Integer; assume A5: b |^ n = 1_G; consider k being Nat such that A6: n = k or n = - k by INT_1:2; per cases by A6; suppose n = k; hence thesis by A1,A5,GROUP_1:def 10; end; suppose A7: n = -k; then k = 0 by A2,A5; hence thesis by A7; end; end; hence thesis; end; assume for n being Integer holds b|^n = 1_G implies n = 0; then for n being Nat holds b |^n = 1_G implies n = 0; hence thesis by GROUP_1:def 10; end; theorem for G st ex a st a <> 1_G holds (for H 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 such that A1: ex a st a <> 1_G; thus (for H 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 proof assume A2: for H holds H = G or H = (1).G; consider b such that A3: b <> 1_G by A1; A4: gr {b} = G by A2,A3,Th7; A5: b is not being_of_order_0 proof assume A6: b is being_of_order_0; then A7: b|^2 <> 1_G by GROUP_1:def 10; not b in gr{b|^2} proof assume b in gr{b|^2}; 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 thesis by INT_1:9; end; then gr{b|^2} <> G; hence contradiction by A2,A7,Th7; end; then consider n being Element of NAT such that A9: n = ord b and b is not 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; ex u,v being Element of NAT st u >1 & v > 1 & n = u * v proof A13: not (n>1 & for m being Nat holds m divides n implies m = 1 or 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 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 as Element of NAT by ORDINAL1:def 12; take u = m; take v = o; u <> 0 proof assume u = 0; then n = 0 * (n div 0) by A16,NAT_D:3; hence contradiction by A10,A11; 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 thesis by A14,A17,A18,A19,XXREAL_0:1; 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 thesis by A2,A11,A23,A24; end; hence thesis by A4,A5,A11,Th11,GR_CY_2:4; 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; let H; reconsider G as finite Group by A25; reconsider 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; per cases by A26,A27,INT_2:def 4; suppose card H = card G; hence thesis by GROUP_2:73; end; suppose card H = 1; hence thesis by GROUP_2:70; end; end; theorem Th15: for G being Group, 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; let x,y,z be Element of G; let A be Subset of G; thus z in x * A * y implies ex a being Element of G st z = x * a * y & a in A proof assume z in x * A * y; 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; thus thesis by A1,A3,A4; end; given a being Element of G such that A5: z = x * a * y and A6: a in A; ex h being Element of G st z = h * y & h in x * A by A5,A6,GROUP_2:27; hence thesis by GROUP_2:28; end; theorem for G being Group, A being non empty Subset of G holds for x being Element of G holds card A = card (x" * A * x) proof let G be Group, A be non empty Subset of G; let x be Element of G; set B = x" * A * x; A is non empty & B is non empty proof set a = the Element of A; x" * a * x in B by Th15; hence thesis; end; then reconsider B as non empty Subset of G; deffunc F(Element 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 = F(a) from FUNCT_2:sch 4; A2: dom f = A by FUNCT_2:def 1; A3: rng f c= B proof let s be object; assume s in rng f; then consider a being object such that A4: a in A and A5: s = f.a by A2,FUNCT_1:def 3; reconsider a as Element of A by A4; s = F(a) by A1,A5; hence thesis by Th15; end; A6: B c= rng f proof let s be object; assume s in B; 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; thus thesis by A1,A7,A8,FUNCT_2:def 1; end; hence thesis by FUNCT_1:def 3; end; reconsider f as Function of A,B by A2,A3,FUNCT_2:2; deffunc FF(Element 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 = FF(b) from FUNCT_2:sch 4; A10: dom g = B by FUNCT_2:def 1; rng g c= A proof let s be object; assume s in rng g; then consider a being object such that A11: a in B and A12: s = g.a by A10,FUNCT_1:def 3; reconsider a as Element of B by A11; A13: s = FF(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 thesis by A15; end; then reconsider 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 such that A17: f.a = f.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 thesis by A17,A20; end; A,B are_equipotent proof take f; thus thesis by A3,A6,A16,FUNCT_2:def 1,GROUP_6:1,XBOOLE_0:def 10; end; hence thesis by CARD_1:5; end; definition let G, H, K; func Double_Cosets (H, K) -> Subset-Family of G means A in it iff ex a st A = H * a * K; existence proof defpred P[set] means ex a st \$1 = H * a * K; ex F being Subset-Family of G st for A being Subset of G holds A in F iff P[A] from SUBSET_1:sch 3; hence thesis; end; uniqueness proof let F1,F2 be Subset-Family of G; defpred P[set] means ex a st \$1 = H * a * K; assume A1: for A holds A in F1 iff P[A]; assume A2: for A holds A in F2 iff P[A]; thus thesis from SUBSET_1:sch 4(A1,A2); end; end; theorem Th17: 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 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 proof assume z in H * x * 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 thesis by A1,A3; 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; ex g1, g2 being Element of G st z = g1 * g2 & g1 in H * x & g2 in K by A5,A4,A6,GROUP_2:104; hence thesis by GROUP_2:94; end; theorem for H, K holds H * x * K = H * y * K or not ex z st z in H * x * K & z in H * y * K proof let H, K; per cases; suppose not ex z st z in H * x * K & z in H * y * K; hence thesis; end; suppose ex z st z in H * x * K & z in H * y * K; then consider z 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 be object st a in H * x * K holds a in H * y * K proof let a be object; assume a in H * x * 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; take k2 * k1" * 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 thesis by A7,A9,A11,A13,A14,GROUP_2:50; end; hence thesis by Th17; end; then A15: H * x * K c= H * y * K; for a be object st a in H * y * K holds a in H * x * K proof let a be object; assume a in H * y * 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; take k1 * k2" * 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 thesis by A4,A16,A18,A20,A21,GROUP_2:50; end; hence thesis by Th17; end; then H * y * K c= H * x * K; hence thesis by A15,XBOOLE_0:def 10; end; end; reserve G for Group; reserve H, B, A for Subgroup of G, D for Subgroup of A; registration let G,A; cluster Left_Cosets A -> non empty; coherence 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: D = A /\ B & G is finite implies index(G,B) >= index(A,D) proof assume that A1: D = A /\ B and A2: G is finite; reconsider LCB = Left_Cosets B as finite non empty set by A2; reconsider LCD = Left_Cosets D as finite non empty set by A2; A3: now let x,y be Element of G; let x9,y9 be Element of A such that A4: x9 = x and A5: y9 = y; A6: y9" = y" by A5,GROUP_2:48; A7: y9"*x9 in A; 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; end; defpred P[set, set] means ex a being Element of G, 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 P[x,y] proof let x be Element of LCD; 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,a,a9; thus thesis by A9; end; consider F being Function of LCD, LCB such that A10: for a being Element of LCD holds P[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 object; assume that A15: x1 in dom F and A16: x2 in dom F; reconsider z1 = x1, z2 = x2 as Element of LCD by A15,A16,FUNCT_2:def 1; A17: ex a being Element of G, a9 being Element of A st ( a = a9)& ( F.z1 = a*B)&( z1 = a9*D) by A10; ex b being Element of G, b9 being Element of A st ( b = b9)& ( F.z2 = b*B)&( z2 = b9*D) by A10; hence thesis by A3,A17; end; then Segm index D c= Segm index B by A11,A12,A13,A14,CARD_1:10; hence thesis by NAT_1:39; end; theorem Th20: for G being finite Group, H be Subgroup of G holds index (G,H) > 0 proof let G be finite Group, H be Subgroup of G; card G = card H * index H by GROUP_2:147; hence thesis; end; theorem for G being Group st G is finite for C being Subgroup of G for A,B being Subgroup of C for D being Subgroup of A st D = A /\ B for E being Subgroup of B st E = A /\ B for F being Subgroup of C st F = A /\ B holds index (C,A), index (C,B) are_coprime implies index (C,B) = index (A,D) & index (C,A) = index (B,E) proof let G such that A1: G is finite; let C be Subgroup of G; let A,B be Subgroup of C; let D be Subgroup of A such that A2: D = A /\ B; let E be Subgroup of B such that A3: E = A /\ B; let F be Subgroup of C such that A4: F = A /\ B; assume that A5: index A, index B are_coprime; 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 qua Integer) divides ((index A qua Integer) * (index D qua Integer)) by INT_1:def 3; then A7: (index B qua Integer) divides (index D qua Integer) 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 qua Integer) * i by A7,INT_1:def 3; 0 <= i by A1,A8,Th20; then reconsider i as Element of NAT by INT_1:3; take i; thus thesis by A8; 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; index D > 0 by A1,Th20; then index B <= index D by A9,NAT_D:7; hence contradiction by A10,A12,XXREAL_0:1; end; (index A qua Integer) divides ((index B qua Integer) * (index E qua Integer)) by A6,INT_1:def 3; then A13: (index A qua Integer) 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 qua Integer) * i by A13,INT_1:def 3; 0 <= i by A1,A14,Th20; then reconsider i as Element of NAT by INT_1:3; take i; thus thesis by A14; 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; index E > 0 by A1,Th20; then index A <= index E by A15,NAT_D:7; hence contradiction by A16,A17,XXREAL_0:1; end; hence thesis by A11; end; theorem Th22: for a being Element of G st a in H holds for j being Integer holds a |^ j in H proof let a be Element of G; assume A1: a in H; let j be Integer; consider k being Nat such that A2: j = k or j = - k by INT_1:2; per cases by A2; suppose A3: j =k; defpred P[Nat] means a |^ \$1 in H; a |^0 = 1_G by GROUP_1:25; then A4: P[ 0 ] by GROUP_2:46; A5: for n being Nat st P[n] holds P[n + 1] proof let n be Nat; assume P[n]; then (a |^ n) * a in H by A1,GROUP_2:50; hence thesis by GROUP_1:34; end; for n being Nat holds P[n] from NAT_1:sch 2(A4,A5); hence thesis by A3; end; suppose A6: j = - k; defpred PP[Nat] means a |^ (- \$1) in H; a |^0 = 1_G by GROUP_1:25; then A7: PP[ 0 ] by GROUP_2:46; A8: for n being Nat st PP[n] holds PP[n +1 ] proof let n be Nat such that A9: PP[n]; 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 thesis; end; for n being Nat holds PP[n] from NAT_1:sch 2(A7,A8); hence thesis by A6; end; end; theorem Th23: for G being strict Group st G <> (1).G ex b being Element of G st b <> 1_G proof let G be strict Group such that A1: G <> (1).G; assume A2: not ex b being Element of G st b <> 1_G; for x,y being Element of G holds x = y proof let x,y be Element of G; x = 1_G by A2; hence thesis by A2; end; then G is trivial; hence contradiction by A1,GROUP_6:12; end; theorem Th24: for G being strict Group for a being Element of G st G = gr{a} for H being strict Subgroup of G st H <> (1).G holds ex k being Nat st 0 < k & a |^k in H proof let G be strict Group; let a be Element of G such that A1: G = gr{a}; let H be strict Subgroup of G; assume H <> (1).G; 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; then c in G by GROUP_2:40; then reconsider c as Element of G; A5: c in gr{a} by A1; ex j being Integer st c = a |^j & j <> 0 proof assume A6: not ex j being Integer st c = a |^j & j <> 0; 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; end; then consider j being Integer such that A9: c = a |^ j and A10: j <> 0; consider n being Nat such that A11: j = n or j = -n by INT_1:2; per cases by A11; suppose j = n; hence thesis by A4,A9,A10; end; suppose A12: j = - n; 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 thesis by A13; end; end; theorem 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; let H be strict Subgroup of G; per cases; suppose H = (1).G; hence thesis; end; suppose A1: H <> (1).G; consider b being Element of G such that A2: the multMagma 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 P[Nat] means 0 < \$1 & b |^\$1 in H; ex k being Nat st P[k] by A1,A2,Th24; then A3: ex k being Nat st P[k]; ex m being Nat st P[m] & for j being Nat st P[j] holds m <= j from NAT_1:sch 5(A3); hence thesis; 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 as Element of H by A5; for a being Element of H holds ex i being Integer st a = c |^ i proof let a be Element of H; 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; then consider j1 being Integer such that A9: a = b |^ j1 by A8,GR_CY_1:5; b |^ j1 in H by A9; hence thesis by A9; 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; take t mod m; thus thesis by A4,NEWTON:64,65,66; end; then consider r,s being Integer such that A12: 0 <= s and A13: s < m and A14: t = m * r + s; reconsider 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: v" * u = (v" * v) * b|^s by A15,GROUP_1:def 3 .= 1_G * b |^ s by GROUP_1:def 5 .= b |^ s by GROUP_1:def 4; v" in H by A16,GROUP_2:51; hence thesis by A10,A17,GROUP_2:50; 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 thesis by A11,A18; end; then H = gr{c} by GR_CY_2:5; hence thesis by GR_CY_2:4; end; end;