:: GROUPP_1 semantic presentation begin theorem Th1: :: GROUPP_1:1 for n being Nat for p being prime Nat st ( for r being Nat holds n <> p |^ r ) holds ex s being Element of NAT st ( s is prime & s divides n & s <> p ) proof let n be Nat; ::_thesis: for p being prime Nat st ( for r being Nat holds n <> p |^ r ) holds ex s being Element of NAT st ( s is prime & s divides n & s <> p ) let p be prime Nat; ::_thesis: ( ( for r being Nat holds n <> p |^ r ) implies ex s being Element of NAT st ( s is prime & s divides n & s <> p ) ) assume A1: for r being Nat holds n <> p |^ r ; ::_thesis: ex s being Element of NAT st ( s is prime & s divides n & s <> p ) percases ( n = 0 or n <> 0 ) ; supposeA2: n = 0 ; ::_thesis: ex s being Element of NAT st ( s is prime & s divides n & s <> p ) percases ( p = 2 or p <> 2 ) ; supposeA3: p = 2 ; ::_thesis: ex s being Element of NAT st ( s is prime & s divides n & s <> p ) take s = 3; ::_thesis: ( s is prime & s divides n & s <> p ) thus s is prime by PEPIN:41; ::_thesis: ( s divides n & s <> p ) thus s divides n by A2, INT_2:12; ::_thesis: s <> p thus s <> p by A3; ::_thesis: verum end; supposeA4: p <> 2 ; ::_thesis: ex s being Element of NAT st ( s is prime & s divides n & s <> p ) take s = 2; ::_thesis: ( s is prime & s divides n & s <> p ) thus s is prime by INT_2:28; ::_thesis: ( s divides n & s <> p ) thus s divides n by A2, INT_2:12; ::_thesis: s <> p thus s <> p by A4; ::_thesis: verum end; end; end; supposeA5: n <> 0 ; ::_thesis: ex s being Element of NAT st ( s is prime & s divides n & s <> p ) A6: p > 1 by INT_2:def_4; reconsider r1 = p |-count n as Element of NAT ; A7: p |^ r1 divides n by A5, A6, NAT_3:def_7; A8: not p |^ (r1 + 1) divides n by A5, A6, NAT_3:def_7; consider s1 being Nat such that A9: n = (p |^ r1) * s1 by A7, NAT_D:def_3; s1 >= 2 proof assume not s1 >= 2 ; ::_thesis: contradiction then s1 < 1 + 1 ; then s1 <= 1 by NAT_1:13; then ( s1 = 0 or s1 = 1 ) by NAT_1:25; hence contradiction by A5, A1, A9; ::_thesis: verum end; then consider s being Element of NAT such that A10: s is prime and A11: s divides s1 by INT_2:31; A12: s1 divides n by A9, NAT_D:def_3; take s ; ::_thesis: ( s is prime & s divides n & s <> p ) s <> p proof assume s = p ; ::_thesis: contradiction then consider s2 being Nat such that A13: s1 = p * s2 by A11, NAT_D:def_3; n = ((p |^ r1) * p) * s2 by A9, A13 .= (p |^ (r1 + 1)) * s2 by NEWTON:6 ; hence contradiction by A8, NAT_D:def_3; ::_thesis: verum end; hence ( s is prime & s divides n & s <> p ) by A10, A11, A12, NAT_D:4; ::_thesis: verum end; end; end; theorem Th2: :: GROUPP_1:2 for p being prime Nat for n, m being Nat st n divides p |^ m holds ex r being Nat st ( n = p |^ r & r <= m ) proof let p be prime Nat; ::_thesis: for n, m being Nat st n divides p |^ m holds ex r being Nat st ( n = p |^ r & r <= m ) let n, m be Nat; ::_thesis: ( n divides p |^ m implies ex r being Nat st ( n = p |^ r & r <= m ) ) assume A1: n divides p |^ m ; ::_thesis: ex r being Nat st ( n = p |^ r & r <= m ) n > 0 proof assume n <= 0 ; ::_thesis: contradiction then n = 0 ; hence contradiction by A1, INT_2:3; ::_thesis: verum end; then n in NatDivisors (p |^ m) by A1, MOEBIUS1:39; then n in { (p |^ k) where k is Element of NAT : k <= m } by NAT_5:19; then consider r being Element of NAT such that A2: ( n = p |^ r & r <= m ) ; take r ; ::_thesis: ( n = p |^ r & r <= m ) thus ( n = p |^ r & r <= m ) by A2; ::_thesis: verum end; theorem Th3: :: GROUPP_1:3 for G being Group for a being Element of G for n being Nat st a |^ n = 1_ G holds (a ") |^ n = 1_ G proof let G be Group; ::_thesis: for a being Element of G for n being Nat st a |^ n = 1_ G holds (a ") |^ n = 1_ G let a be Element of G; ::_thesis: for n being Nat st a |^ n = 1_ G holds (a ") |^ n = 1_ G let n be Nat; ::_thesis: ( a |^ n = 1_ G implies (a ") |^ n = 1_ G ) assume a |^ n = 1_ G ; ::_thesis: (a ") |^ n = 1_ G then (a ") |^ n = (1_ G) " by GROUP_1:37 .= 1_ G by GROUP_1:8 ; hence (a ") |^ n = 1_ G ; ::_thesis: verum end; theorem Th4: :: GROUPP_1:4 for G being Group for a being Element of G for n being Nat st (a ") |^ n = 1_ G holds a |^ n = 1_ G proof let G be Group; ::_thesis: for a being Element of G for n being Nat st (a ") |^ n = 1_ G holds a |^ n = 1_ G let a be Element of G; ::_thesis: for n being Nat st (a ") |^ n = 1_ G holds a |^ n = 1_ G let n be Nat; ::_thesis: ( (a ") |^ n = 1_ G implies a |^ n = 1_ G ) (a ") " = a ; hence ( (a ") |^ n = 1_ G implies a |^ n = 1_ G ) by Th3; ::_thesis: verum end; theorem Th5: :: GROUPP_1:5 for G being Group for a being Element of G holds ord (a ") = ord a proof let G be Group; ::_thesis: for a being Element of G holds ord (a ") = ord a let a be Element of G; ::_thesis: ord (a ") = ord a a |^ (ord a) = 1_ G by GROUP_1:41; then (a ") |^ (ord a) = 1_ G by Th3; then A1: ord (a ") divides ord a by GROUP_1:44; (a ") |^ (ord (a ")) = 1_ G by GROUP_1:41; then a |^ (ord (a ")) = 1_ G by Th4; then ord a divides ord (a ") by GROUP_1:44; hence ord (a ") = ord a by A1, NAT_D:5; ::_thesis: verum end; theorem Th6: :: GROUPP_1:6 for G being Group for a, b being Element of G holds ord (a |^ b) = ord a proof let G be Group; ::_thesis: for a, b being Element of G holds ord (a |^ b) = ord a let a, b be Element of G; ::_thesis: ord (a |^ b) = ord a (a |^ b) |^ (ord a) = (a |^ (ord a)) |^ b by GROUP_3:27 .= (1_ G) |^ b by GROUP_1:41 .= 1_ G by GROUP_3:17 ; then A1: ord (a |^ b) divides ord a by GROUP_1:44; (a |^ (ord (a |^ b))) |^ b = (a |^ b) |^ (ord (a |^ b)) by GROUP_3:27 .= 1_ G by GROUP_1:41 ; then ord a divides ord (a |^ b) by GROUP_1:44, GROUP_3:18; hence ord (a |^ b) = ord a by A1, NAT_D:5; ::_thesis: verum end; theorem Th7: :: GROUPP_1:7 for G being Group for N being Subgroup of G for a, b being Element of G st N is normal & b in N holds for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) proof let G be Group; ::_thesis: for N being Subgroup of G for a, b being Element of G st N is normal & b in N holds for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) let N be Subgroup of G; ::_thesis: for a, b being Element of G st N is normal & b in N holds for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) let a, b be Element of G; ::_thesis: ( N is normal & b in N implies for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) ) assume A1: ( N is normal & b in N ) ; ::_thesis: for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) defpred S1[ Nat] means for n being Nat ex g being Element of G st ( g in N & (a * b) |^ \$1 = (a |^ \$1) * g ); A2: (a * b) |^ 0 = 1_ G by GROUP_1:25; (a |^ 0) * (1_ G) = (1_ G) * (1_ G) by GROUP_1:25 .= 1_ G by GROUP_1:def_4 ; then A3: S1[ 0 ] by A2, GROUP_2:46; A4: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then consider g1 being Element of G such that A5: ( g1 in N & (a * b) |^ n = (a |^ n) * g1 ) ; A6: (a * b) |^ (n + 1) = ((a |^ n) * g1) * (a * b) by A5, GROUP_1:34 .= (a |^ n) * (g1 * (a * b)) by GROUP_1:def_3 .= (a |^ n) * ((g1 * a) * b) by GROUP_1:def_3 ; a * N = N * a by A1, GROUP_3:117; then g1 * a in a * N by A5, GROUP_2:104; then consider g2 being Element of G such that A7: ( g1 * a = a * g2 & g2 in N ) by GROUP_2:103; (g1 * a) * b = a * (g2 * b) by A7, GROUP_1:def_3; then (a |^ n) * ((g1 * a) * b) = ((a |^ n) * a) * (g2 * b) by GROUP_1:def_3 .= (a |^ (n + 1)) * (g2 * b) by GROUP_1:34 ; hence S1[n + 1] by A1, A6, A7, GROUP_2:50; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4); hence for n being Nat ex g being Element of G st ( g in N & (a * b) |^ n = (a |^ n) * g ) ; ::_thesis: verum end; theorem Th8: :: GROUPP_1:8 for G being Group for N being normal Subgroup of G for a being Element of G for S being Element of (G ./. N) st S = a * N holds for n being Nat holds S |^ n = (a |^ n) * N proof let G be Group; ::_thesis: for N being normal Subgroup of G for a being Element of G for S being Element of (G ./. N) st S = a * N holds for n being Nat holds S |^ n = (a |^ n) * N let N be normal Subgroup of G; ::_thesis: for a being Element of G for S being Element of (G ./. N) st S = a * N holds for n being Nat holds S |^ n = (a |^ n) * N let a be Element of G; ::_thesis: for S being Element of (G ./. N) st S = a * N holds for n being Nat holds S |^ n = (a |^ n) * N let S be Element of (G ./. N); ::_thesis: ( S = a * N implies for n being Nat holds S |^ n = (a |^ n) * N ) assume A1: S = a * N ; ::_thesis: for n being Nat holds S |^ n = (a |^ n) * N defpred S1[ Nat] means for n being Nat holds S |^ \$1 = (a |^ \$1) * N; A2: S |^ 0 = 1_ (G ./. N) by GROUP_1:25; (a |^ 0) * N = (1_ G) * N by GROUP_1:25 .= carr N by GROUP_2:109 ; then A3: S1[ 0 ] by A2, GROUP_6:24; A4: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A5: S1[n] ; ::_thesis: S1[n + 1] S |^ (n + 1) = (S |^ n) * S by GROUP_1:34 .= (@ (S |^ n)) * (@ S) by GROUP_6:def_3 .= ((a |^ n) * N) * (a * N) by A1, A5 .= ((a |^ n) * a) * N by GROUP_11:1 .= (a |^ (n + 1)) * N by GROUP_1:34 ; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4); hence for n being Nat holds S |^ n = (a |^ n) * N ; ::_thesis: verum end; theorem Th9: :: GROUPP_1:9 for G being Group for H being Subgroup of G for a, b being Element of G st a * H = b * H holds ex h being Element of G st ( a = b * h & h in H ) proof let G be Group; ::_thesis: for H being Subgroup of G for a, b being Element of G st a * H = b * H holds ex h being Element of G st ( a = b * h & h in H ) let H be Subgroup of G; ::_thesis: for a, b being Element of G st a * H = b * H holds ex h being Element of G st ( a = b * h & h in H ) let a, b be Element of G; ::_thesis: ( a * H = b * H implies ex h being Element of G st ( a = b * h & h in H ) ) a in a * H by GROUP_2:108; hence ( a * H = b * H implies ex h being Element of G st ( a = b * h & h in H ) ) by GROUP_2:103; ::_thesis: verum end; theorem Th10: :: GROUPP_1:10 for G being finite Group for N being normal Subgroup of G st N is Subgroup of center G & G ./. N is cyclic holds G is commutative proof let G be finite Group; ::_thesis: for N being normal Subgroup of G st N is Subgroup of center G & G ./. N is cyclic holds G is commutative let N be normal Subgroup of G; ::_thesis: ( N is Subgroup of center G & G ./. N is cyclic implies G is commutative ) assume that A1: N is Subgroup of center G and A2: G ./. N is cyclic ; ::_thesis: G is commutative reconsider I = G ./. N as finite Group ; consider S being Element of I such that A3: for T being Element of I ex n being Nat st T = S |^ n by A2, GR_CY_1:18; consider a1 being Element of G such that A4: ( S = a1 * N & S = N * a1 ) by GROUP_6:21; for a, b being Element of G holds a * b = b * a proof let a, b be Element of G; ::_thesis: a * b = b * a A5: ( a * N is Element of I & b * N is Element of I ) by GROUP_6:22; then consider r1 being Nat such that A6: a * N = S |^ r1 by A3; a * N = (a1 |^ r1) * N by A4, Th8, A6; then consider c1 being Element of G such that A7: ( a = (a1 |^ r1) * c1 & c1 in N ) by Th9; A8: c1 in center G by A1, A7, GROUP_2:40; consider r2 being Nat such that A9: b * N = S |^ r2 by A3, A5; b * N = (a1 |^ r2) * N by A4, Th8, A9; then consider c2 being Element of G such that A10: ( b = (a1 |^ r2) * c2 & c2 in N ) by Th9; A11: c2 in center G by A1, A10, GROUP_2:40; a * b = (a1 |^ r1) * (c1 * ((a1 |^ r2) * c2)) by A7, A10, GROUP_1:def_3 .= (a1 |^ r1) * (((a1 |^ r2) * c2) * c1) by A8, GROUP_5:77 .= (a1 |^ r1) * ((a1 |^ r2) * (c2 * c1)) by GROUP_1:def_3 .= ((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1) by GROUP_1:def_3 .= (a1 |^ (r1 + r2)) * (c2 * c1) by GROUP_1:33 .= ((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1) by GROUP_1:33 .= (a1 |^ r2) * ((a1 |^ r1) * (c2 * c1)) by GROUP_1:def_3 .= (a1 |^ r2) * (((a1 |^ r1) * c2) * c1) by GROUP_1:def_3 .= (a1 |^ r2) * ((c2 * (a1 |^ r1)) * c1) by A11, GROUP_5:77 .= (a1 |^ r2) * (c2 * ((a1 |^ r1) * c1)) by GROUP_1:def_3 .= b * a by A7, A10, GROUP_1:def_3 ; hence a * b = b * a ; ::_thesis: verum end; hence G is commutative by GROUP_1:def_12; ::_thesis: verum end; theorem :: GROUPP_1:11 for G being finite Group for N being normal Subgroup of G st N = center G & G ./. N is cyclic holds G is commutative proof let G be finite Group; ::_thesis: for N being normal Subgroup of G st N = center G & G ./. N is cyclic holds G is commutative let N be normal Subgroup of G; ::_thesis: ( N = center G & G ./. N is cyclic implies G is commutative ) assume A1: ( N = center G & G ./. N is cyclic ) ; ::_thesis: G is commutative then N is Subgroup of center G by GROUP_2:54; hence G is commutative by A1, Th10; ::_thesis: verum end; theorem :: GROUPP_1:12 for G being finite Group for H being Subgroup of G st card H <> card G holds ex a being Element of G st not a in H proof let G be finite Group; ::_thesis: for H being Subgroup of G st card H <> card G holds ex a being Element of G st not a in H let H be Subgroup of G; ::_thesis: ( card H <> card G implies ex a being Element of G st not a in H ) assume A1: card H <> card G ; ::_thesis: not for a being Element of G holds a in H assume for a being Element of G holds a in H ; ::_thesis: contradiction then multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by GROUP_2:62; hence contradiction by A1; ::_thesis: verum end; definition let p be Nat; let G be Group; let a be Element of G; attra is p -power means :Def1: :: GROUPP_1:def 1 ex r being Nat st ord a = p |^ r; end; :: deftheorem Def1 defines -power GROUPP_1:def_1_:_ for p being Nat for G being Group for a being Element of G holds ( a is p -power iff ex r being Nat st ord a = p |^ r ); theorem Th13: :: GROUPP_1:13 for G being Group for m being Nat holds 1_ G is m -power proof let G be Group; ::_thesis: for m being Nat holds 1_ G is m -power let m be Nat; ::_thesis: 1_ G is m -power A1: ord (1_ G) = 1 by GROUP_1:42; m |^ 0 = 1 by NEWTON:4; hence 1_ G is m -power by A1, Def1; ::_thesis: verum end; registration let G be Group; let m be Nat; clusterm -power for Element of the carrier of G; existence ex b1 being Element of G st b1 is m -power proof take 1_ G ; ::_thesis: 1_ G is m -power thus 1_ G is m -power by Th13; ::_thesis: verum end; end; registration let p be prime Nat; let G be Group; let a be p -power Element of G; clustera " -> p -power ; coherence a " is p -power proof consider n being Nat such that A1: ord a = p |^ n by Def1; ord (a ") = p |^ n by A1, Th5; hence a " is p -power by Def1; ::_thesis: verum end; end; theorem :: GROUPP_1:14 for G being Group for a, b being Element of G for p being prime Nat st a |^ b is p -power holds a is p -power proof let G be Group; ::_thesis: for a, b being Element of G for p being prime Nat st a |^ b is p -power holds a is p -power let a, b be Element of G; ::_thesis: for p being prime Nat st a |^ b is p -power holds a is p -power let p be prime Nat; ::_thesis: ( a |^ b is p -power implies a is p -power ) assume a |^ b is p -power ; ::_thesis: a is p -power then consider r being Nat such that A1: ord (a |^ b) = p |^ r by Def1; ord a = p |^ r by A1, Th6; hence a is p -power by Def1; ::_thesis: verum end; registration let p be prime Nat; let G be Group; let b be Element of G; let a be p -power Element of G; clustera |^ b -> p -power ; coherence a |^ b is p -power proof consider n being Nat such that A1: ord a = p |^ n by Def1; ord (a |^ b) = p |^ n by A1, Th6; hence a |^ b is p -power by Def1; ::_thesis: verum end; end; registration let p be prime Nat; let G be commutative Group; let a, b be p -power Element of G; clustera * b -> p -power ; coherence a * b is p -power proof consider n being Nat such that A1: ord a = p |^ n by Def1; consider m being Nat such that A2: ord b = p |^ m by Def1; A3: a |^ (p |^ (n + m)) = a |^ ((p |^ n) * (p |^ m)) by NEWTON:8 .= (a |^ (p |^ n)) |^ (p |^ m) by GROUP_1:35 .= (1_ G) |^ (p |^ m) by A1, GROUP_1:41 .= 1_ G by GROUP_1:31 ; b |^ (p |^ (n + m)) = b |^ ((p |^ m) * (p |^ n)) by NEWTON:8 .= (b |^ (p |^ m)) |^ (p |^ n) by GROUP_1:35 .= (1_ G) |^ (p |^ n) by A2, GROUP_1:41 .= 1_ G by GROUP_1:31 ; then (a * b) |^ (p |^ (n + m)) = (1_ G) * (1_ G) by A3, GROUP_1:48 .= 1_ G by GROUP_1:def_4 ; then consider r being Nat such that A4: ( ord (a * b) = p |^ r & r <= n + m ) by Th2, GROUP_1:44; take r ; :: according to GROUPP_1:def_1 ::_thesis: ord (a * b) = p |^ r thus ord (a * b) = p |^ r by A4; ::_thesis: verum end; end; registration let p be prime Nat; let G be finite p -group Group; cluster -> p -power for Element of the carrier of G; coherence for b1 being Element of G holds b1 is p -power proof let a be Element of G; ::_thesis: a is p -power consider m being Nat such that A1: card G = p |^ m by GROUP_10:def_17; ex r being Nat st ( ord a = p |^ r & r <= m ) by A1, Th2, GR_CY_1:8; hence a is p -power by Def1; ::_thesis: verum end; end; theorem Th15: :: GROUPP_1:15 for p being prime Nat for G being finite Group for H being Subgroup of G for a being Element of G st H is p -group & a in H holds a is p -power proof let p be prime Nat; ::_thesis: for G being finite Group for H being Subgroup of G for a being Element of G st H is p -group & a in H holds a is p -power let G be finite Group; ::_thesis: for H being Subgroup of G for a being Element of G st H is p -group & a in H holds a is p -power let H be Subgroup of G; ::_thesis: for a being Element of G st H is p -group & a in H holds a is p -power let a be Element of G; ::_thesis: ( H is p -group & a in H implies a is p -power ) assume that A1: H is p -group and A2: a in H ; ::_thesis: a is p -power a is Element of H by A2, STRUCT_0:def_5; then consider b being Element of H such that A3: b = a ; consider r being Nat such that A4: ord b = p |^ r by A1, Def1; ord a = p |^ r by A3, A4, GROUP_8:5; hence a is p -power by Def1; ::_thesis: verum end; registration let p be prime Nat; let G be finite p -group Group; cluster -> p -group for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is p -group proof let H be Subgroup of G; ::_thesis: H is p -group consider m being Nat such that A1: card G = p |^ m by GROUP_10:def_17; ex r being Nat st ( card H = p |^ r & r <= m ) by A1, Th2, GROUP_2:148; hence H is p -group by GROUP_10:def_17; ::_thesis: verum end; end; theorem Th16: :: GROUPP_1:16 for G being Group for p being prime Nat holds (1). G is p -group proof let G be Group; ::_thesis: for p being prime Nat holds (1). G is p -group let p be prime Nat; ::_thesis: (1). G is p -group take 0 ; :: according to GROUP_10:def_17 ::_thesis: card ((1). G) = p |^ 0 thus card ((1). G) = 1 by GROUP_2:69 .= p |^ 0 by NEWTON:4 ; ::_thesis: verum end; registration let p be prime Nat; let G be Group; cluster non empty unital Group-like associative p -group for Subgroup of G; existence ex b1 being Subgroup of G st b1 is p -group proof take (1). G ; ::_thesis: (1). G is p -group thus (1). G is p -group by Th16; ::_thesis: verum end; end; registration let p be prime Nat; let G be finite Group; let G1 be p -group Subgroup of G; let G2 be Subgroup of G; clusterG1 /\ G2 -> p -group ; coherence G1 /\ G2 is p -group proof reconsider H1 = G1 /\ G2 as Subgroup of G1 by GROUP_2:88; H1 is p -group ; hence G1 /\ G2 is p -group ; ::_thesis: verum end; clusterG2 /\ G1 -> p -group ; coherence G2 /\ G1 is p -group ; end; theorem Th17: :: GROUPP_1:17 for p being prime Nat for G being finite Group st ( for a being Element of G holds a is p -power ) holds G is p -group proof let p be prime Nat; ::_thesis: for G being finite Group st ( for a being Element of G holds a is p -power ) holds G is p -group let G be finite Group; ::_thesis: ( ( for a being Element of G holds a is p -power ) implies G is p -group ) assume A1: for a being Element of G holds a is p -power ; ::_thesis: G is p -group assume not G is p -group ; ::_thesis: contradiction then for r being Nat holds card G <> p |^ r by GROUP_10:def_17; then consider s being Element of NAT such that A2: ( s is prime & s divides card G ) and A3: s <> p by Th1; consider b being Element of G such that A4: ord b = s by A2, GROUP_10:11; b is p -power by A1; then ex r1 being Nat st ord b = p |^ r1 by Def1; hence contradiction by A2, A4, A3, NAT_3:6; ::_thesis: verum end; registration let p be prime Nat; let G be finite p -group Group; let N be normal Subgroup of G; clusterG ./. N -> p -group ; coherence G ./. N is p -group proof consider r being Nat such that A1: card G = p |^ r by GROUP_10:def_17; A2: card G = (card N) * (index N) by GROUP_2:147; A3: card (G ./. N) = index N by GROUP_6:27; reconsider n = card (G ./. N) as Nat ; n divides p |^ r by A1, A2, A3, NAT_D:def_3; then ex r1 being Nat st ( n = p |^ r1 & r1 <= r ) by Th2; hence G ./. N is p -group by GROUP_10:def_17; ::_thesis: verum end; end; theorem :: GROUPP_1:18 for p being prime Nat for G being finite Group for N being normal Subgroup of G st N is p -group & G ./. N is p -group holds G is p -group proof let p be prime Nat; ::_thesis: for G being finite Group for N being normal Subgroup of G st N is p -group & G ./. N is p -group holds G is p -group let G be finite Group; ::_thesis: for N being normal Subgroup of G st N is p -group & G ./. N is p -group holds G is p -group let N be normal Subgroup of G; ::_thesis: ( N is p -group & G ./. N is p -group implies G is p -group ) assume that A1: N is p -group and A2: G ./. N is p -group ; ::_thesis: G is p -group consider r1 being Nat such that A3: card N = p |^ r1 by A1, GROUP_10:def_17; consider r2 being Nat such that A4: card (G ./. N) = p |^ r2 by A2, GROUP_10:def_17; card (G ./. N) = index N by GROUP_6:27; then card G = (p |^ r1) * (p |^ r2) by A3, A4, GROUP_2:147 .= p |^ (r1 + r2) by NEWTON:8 ; hence G is p -group by GROUP_10:def_17; ::_thesis: verum end; theorem Th19: :: GROUPP_1:19 for p being prime Nat for G being finite commutative Group for H, H1, H2 being Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 holds H is p -group proof let p be prime Nat; ::_thesis: for G being finite commutative Group for H, H1, H2 being Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 holds H is p -group let G be finite commutative Group; ::_thesis: for H, H1, H2 being Subgroup of G st H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 holds H is p -group let H, H1, H2 be Subgroup of G; ::_thesis: ( H1 is p -group & H2 is p -group & the carrier of H = H1 * H2 implies H is p -group ) assume that A1: ( H1 is p -group & H2 is p -group ) and A2: the carrier of H = H1 * H2 ; ::_thesis: H is p -group for a being Element of H holds a is p -power proof let a be Element of H; ::_thesis: a is p -power a in H1 * H2 by A2; then consider b1, b2 being Element of G such that A3: ( a = b1 * b2 & b1 in H1 & b2 in H2 ) by GROUP_11:6; ( b1 is p -power & b2 is p -power ) by A1, A3, Th15; then consider r being Nat such that A4: ord (b1 * b2) = p |^ r by Def1; ord a = p |^ r by A3, A4, GROUP_8:5; hence a is p -power by Def1; ::_thesis: verum end; hence H is p -group by Th17; ::_thesis: verum end; theorem Th20: :: GROUPP_1:20 for p being prime Nat for G being finite Group for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -group ) proof let p be prime Nat; ::_thesis: for G being finite Group for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -group ) let G be finite Group; ::_thesis: for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -group ) let H, N be Subgroup of G; ::_thesis: ( N is normal Subgroup of G & H is p -group & N is p -group implies ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -group ) ) assume that A1: N is normal Subgroup of G and A2: ( H is p -group & N is p -group ) ; ::_thesis: ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -group ) H * N = N * H by A1, GROUP_5:8; then consider P being strict Subgroup of G such that A3: the carrier of P = H * N by GROUP_2:78; A4: for a being Element of P holds a is p -power proof let a be Element of P; ::_thesis: a is p -power a in H * N by A3; then consider b, c being Element of G such that A5: ( a = b * c & b in H & c in N ) by GROUP_11:6; b is p -power by A5, A2, Th15; then consider n being Nat such that A6: ord b = p |^ n by Def1; A7: b |^ (p |^ n) = 1_ G by A6, GROUP_1:41; consider d being Element of G such that A8: ( d in N & (b * c) |^ (p |^ n) = (b |^ (p |^ n)) * d ) by A1, A5, Th7; d is p -power by A2, A8, Th15; then consider m being Nat such that A9: ord d = p |^ m by Def1; A10: d |^ (p |^ m) = 1_ G by A9, GROUP_1:41; A11: a |^ (p |^ (n + m)) = (b * c) |^ (p |^ (n + m)) by A5, GROUP_8:4 .= (b * c) |^ ((p |^ n) * (p |^ m)) by NEWTON:8 .= ((b * c) |^ (p |^ n)) |^ (p |^ m) by GROUP_1:35 .= 1_ G by A7, A8, A10, GROUP_1:def_4 ; reconsider a1 = a as Element of G by GROUP_2:42; a1 |^ (p |^ (n + m)) = 1_ G by A11, GROUP_8:4; then consider r being Nat such that A12: ( ord a1 = p |^ r & r <= n + m ) by Th2, GROUP_1:44; ord a = p |^ r by A12, GROUP_8:5; hence a is p -power by Def1; ::_thesis: verum end; take P ; ::_thesis: ( the carrier of P = H * N & P is p -group ) thus ( the carrier of P = H * N & P is p -group ) by A3, A4, Th17; ::_thesis: verum end; theorem Th21: :: GROUPP_1:21 for p being prime Nat for G being finite Group for N1, N2 being normal Subgroup of G st N1 is p -group & N2 is p -group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) proof let p be prime Nat; ::_thesis: for G being finite Group for N1, N2 being normal Subgroup of G st N1 is p -group & N2 is p -group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) let G be finite Group; ::_thesis: for N1, N2 being normal Subgroup of G st N1 is p -group & N2 is p -group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) let N1, N2 be normal Subgroup of G; ::_thesis: ( N1 is p -group & N2 is p -group implies ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) ) assume ( N1 is p -group & N2 is p -group ) ; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) then consider N being strict Subgroup of G such that A1: ( the carrier of N = N1 * N2 & N is p -group ) by Th20; for x, y being Element of G st y in N holds (x * y) * (x ") in N proof let x, y be Element of G; ::_thesis: ( y in N implies (x * y) * (x ") in N ) assume y in N ; ::_thesis: (x * y) * (x ") in N then y in the carrier of N by STRUCT_0:def_5; then consider a, b being Element of G such that A2: ( y = a * b & a in N1 & b in N2 ) by A1, GROUP_11:6; A3: (x * y) * (x ") = ((x * a) * b) * (x ") by A2, GROUP_1:def_3 .= (x * a) * (b * (x ")) by GROUP_1:def_3 .= ((x * a) * (1_ G)) * (b * (x ")) by GROUP_1:def_4 .= ((x * a) * ((x ") * x)) * (b * (x ")) by GROUP_1:def_5 .= (((x * a) * (x ")) * x) * (b * (x ")) by GROUP_1:def_3 .= ((x * a) * (x ")) * (x * (b * (x "))) by GROUP_1:def_3 .= ((x * a) * (x ")) * ((x * b) * (x ")) by GROUP_1:def_3 ; ( (x * a) * (x ") in N1 & (x * b) * (x ") in N2 ) by A2, GROUP_11:4; then (x * y) * (x ") in N1 * N2 by A3, GROUP_11:6; hence (x * y) * (x ") in N by A1, STRUCT_0:def_5; ::_thesis: verum end; then N is normal Subgroup of G by GROUP_11:5; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -group ) by A1; ::_thesis: verum end; registration let p be prime Nat; let G be finite p -group Group; let H be finite Group; let g be Homomorphism of G,H; cluster Image g -> p -group ; coherence Image g is p -group proof for h being Element of (Image g) holds h is p -power proof let h be Element of (Image g); ::_thesis: h is p -power h in Image g by STRUCT_0:def_5; then consider a being Element of G such that A1: h = g . a by GROUP_6:45; consider n being Nat such that A2: ord a = p |^ n by Def1; A3: g . (a |^ (p |^ n)) = (g . a) |^ (p |^ n) by GROUP_6:37 .= h |^ (p |^ n) by A1, GROUP_8:4 ; A4: g . (a |^ (p |^ n)) = g . (1_ G) by A2, GROUP_1:41 .= 1_ H by GROUP_6:31 ; reconsider h1 = h as Element of H by GROUP_2:42; h1 |^ (p |^ n) = 1_ H by A3, A4, GROUP_8:4; then consider r being Nat such that A5: ( ord h1 = p |^ r & r <= n ) by Th2, GROUP_1:44; ord h = p |^ r by A5, GROUP_8:5; hence h is p -power by Def1; ::_thesis: verum end; hence Image g is p -group by Th17; ::_thesis: verum end; end; theorem Th22: :: GROUPP_1:22 for p being prime Nat for G, H being strict Group st G,H are_isomorphic & G is p -group holds H is p -group proof let p be prime Nat; ::_thesis: for G, H being strict Group st G,H are_isomorphic & G is p -group holds H is p -group let G, H be strict Group; ::_thesis: ( G,H are_isomorphic & G is p -group implies H is p -group ) assume that A1: G,H are_isomorphic and A2: G is p -group ; ::_thesis: H is p -group consider r being Nat such that A3: card G = p |^ r by A2, GROUP_10:def_17; card H = p |^ r by A1, A3, GROUP_6:73; hence H is p -group by GROUP_10:def_17; ::_thesis: verum end; definition let p be prime Nat; let G be Group; assume A1: G is p -group ; func expon (G,p) -> Nat means :Def2: :: GROUPP_1:def 2 card G = p |^ it; existence ex b1 being Nat st card G = p |^ b1 by A1, GROUP_10:def_17; uniqueness for b1, b2 being Nat st card G = p |^ b1 & card G = p |^ b2 holds b1 = b2 proof let a, b be Nat; ::_thesis: ( card G = p |^ a & card G = p |^ b implies a = b ) assume that A1: card G = p |^ a and A2: card G = p |^ b ; ::_thesis: a = b p > 1 by INT_2:def_4; hence a = b by A1, A2, PEPIN:30; ::_thesis: verum end; end; :: deftheorem Def2 defines expon GROUPP_1:def_2_:_ for p being prime Nat for G being Group st G is p -group holds for b3 being Nat holds ( b3 = expon (G,p) iff card G = p |^ b3 ); definition let p be prime Nat; let G be Group; :: original: expon redefine func expon (G,p) -> Element of NAT ; coherence expon (G,p) is Element of NAT by ORDINAL1:def_12; end; theorem :: GROUPP_1:23 for p being prime Nat for G being finite Group for H being Subgroup of G st G is p -group holds expon (H,p) <= expon (G,p) proof let p be prime Nat; ::_thesis: for G being finite Group for H being Subgroup of G st G is p -group holds expon (H,p) <= expon (G,p) let G be finite Group; ::_thesis: for H being Subgroup of G st G is p -group holds expon (H,p) <= expon (G,p) let H be Subgroup of G; ::_thesis: ( G is p -group implies expon (H,p) <= expon (G,p) ) assume A1: G is p -group ; ::_thesis: expon (H,p) <= expon (G,p) then card G = p |^ (expon (G,p)) by Def2; then ex r being Nat st ( card H = p |^ r & r <= expon (G,p) ) by Th2, GROUP_2:148; hence expon (H,p) <= expon (G,p) by A1, Def2; ::_thesis: verum end; theorem Th24: :: GROUPP_1:24 for p being prime Nat for G being finite strict Group st G is p -group & expon (G,p) = 0 holds G = (1). G proof let p be prime Nat; ::_thesis: for G being finite strict Group st G is p -group & expon (G,p) = 0 holds G = (1). G let G be finite strict Group; ::_thesis: ( G is p -group & expon (G,p) = 0 implies G = (1). G ) assume ( G is p -group & expon (G,p) = 0 ) ; ::_thesis: G = (1). G then A1: card G = p |^ 0 by Def2 .= 1 by NEWTON:4 ; card ((1). G) = 1 by GROUP_2:69; hence G = (1). G by A1, GROUP_2:73; ::_thesis: verum end; theorem Th25: :: GROUPP_1:25 for p being prime Nat for G being finite strict Group st G is p -group & expon (G,p) = 1 holds G is cyclic proof let p be prime Nat; ::_thesis: for G being finite strict Group st G is p -group & expon (G,p) = 1 holds G is cyclic let G be finite strict Group; ::_thesis: ( G is p -group & expon (G,p) = 1 implies G is cyclic ) assume ( G is p -group & expon (G,p) = 1 ) ; ::_thesis: G is cyclic then card G = p |^ 1 by Def2 .= p by NEWTON:5 ; hence G is cyclic by GR_CY_1:21; ::_thesis: verum end; theorem :: GROUPP_1:26 for G being finite Group for p being prime Nat for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds G is commutative proof let G be finite Group; ::_thesis: for p being prime Nat for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds G is commutative let p be prime Nat; ::_thesis: for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds G is commutative let a be Element of G; ::_thesis: ( G is p -group & expon (G,p) = 2 & ord a = p |^ 2 implies G is commutative ) assume that A1: ( G is p -group & expon (G,p) = 2 ) and A2: ord a = p |^ 2 ; ::_thesis: G is commutative card G = p |^ 2 by A1, Def2; then G is cyclic by A2, GR_CY_1:19; hence G is commutative ; ::_thesis: verum end; begin definition let p be Nat; let G be Group; attrG is p -commutative-group-like means :Def3: :: GROUPP_1:def 3 for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p); end; :: deftheorem Def3 defines -commutative-group-like GROUPP_1:def_3_:_ for p being Nat for G being Group holds ( G is p -commutative-group-like iff for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p) ); definition let p be Nat; let G be Group; attrG is p -commutative-group means :Def4: :: GROUPP_1:def 4 ( G is p -group & G is p -commutative-group-like ); end; :: deftheorem Def4 defines -commutative-group GROUPP_1:def_4_:_ for p being Nat for G being Group holds ( G is p -commutative-group iff ( G is p -group & G is p -commutative-group-like ) ); registration let p be Nat; cluster non empty Group-like associative p -commutative-group -> p -group p -commutative-group-like for multMagma ; coherence for b1 being Group st b1 is p -commutative-group holds ( b1 is p -group & b1 is p -commutative-group-like ) by Def4; cluster non empty Group-like associative p -group p -commutative-group-like -> p -commutative-group for multMagma ; coherence for b1 being Group st b1 is p -group & b1 is p -commutative-group-like holds b1 is p -commutative-group by Def4; end; theorem Th27: :: GROUPP_1:27 for G being Group for p being prime Nat holds (1). G is p -commutative-group-like proof let G be Group; ::_thesis: for p being prime Nat holds (1). G is p -commutative-group-like let p be prime Nat; ::_thesis: (1). G is p -commutative-group-like let a, b be Element of ((1). G); :: according to GROUPP_1:def_3 ::_thesis: (a * b) |^ p = (a |^ p) * (b |^ p) A1: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7; hence (a * b) |^ p = 1_ G by TARSKI:def_1 .= (a |^ p) * (b |^ p) by A1, TARSKI:def_1 ; ::_thesis: verum end; registration let p be prime Nat; cluster non empty finite unital Group-like associative commutative cyclic p -commutative-group for multMagma ; existence ex b1 being Group st ( b1 is p -commutative-group & b1 is finite & b1 is cyclic & b1 is commutative ) proof take (1). the Group ; ::_thesis: ( (1). the Group is p -commutative-group & (1). the Group is finite & (1). the Group is cyclic & (1). the Group is commutative ) ( (1). the Group is p -commutative-group-like & (1). the Group is p -group ) by Th16, Th27; hence ( (1). the Group is p -commutative-group & (1). the Group is finite & (1). the Group is cyclic & (1). the Group is commutative ) ; ::_thesis: verum end; end; registration let p be prime Nat; let G be finite p -commutative-group-like Group; cluster -> p -commutative-group-like for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is p -commutative-group-like proof let H be Subgroup of G; ::_thesis: H is p -commutative-group-like let a, b be Element of H; :: according to GROUPP_1:def_3 ::_thesis: (a * b) |^ p = (a |^ p) * (b |^ p) reconsider a2 = a, b2 = b as Element of G by GROUP_2:42; A1: a * b = a2 * b2 by GROUP_8:2; A2: ( a |^ p = a2 |^ p & b |^ p = b2 |^ p ) by GROUP_8:4; thus (a * b) |^ p = (a2 * b2) |^ p by A1, GROUP_8:4 .= (a2 |^ p) * (b2 |^ p) by Def3 .= (a |^ p) * (b |^ p) by A2, GROUP_8:2 ; ::_thesis: verum end; end; registration let p be prime Nat; cluster non empty finite Group-like associative commutative p -group -> p -commutative-group for multMagma ; coherence for b1 being Group st b1 is p -group & b1 is finite & b1 is commutative holds b1 is p -commutative-group proof let G be Group; ::_thesis: ( G is p -group & G is finite & G is commutative implies G is p -commutative-group ) assume A1: ( G is p -group & G is finite & G is commutative ) ; ::_thesis: G is p -commutative-group for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p) by A1, GROUP_1:48; then G is p -commutative-group-like by Def3; hence G is p -commutative-group by A1; ::_thesis: verum end; end; theorem :: GROUPP_1:28 for p being prime Nat for G being finite strict Group st card G = p holds G is p -commutative-group proof let p be prime Nat; ::_thesis: for G being finite strict Group st card G = p holds G is p -commutative-group let G be finite strict Group; ::_thesis: ( card G = p implies G is p -commutative-group ) assume A1: card G = p ; ::_thesis: G is p -commutative-group p = p |^ 1 by NEWTON:5; then A2: G is p -group by A1, GROUP_10:def_17; G is cyclic Group by A1, GR_CY_1:21; hence G is p -commutative-group by A2; ::_thesis: verum end; registration let p be prime Nat; let G be Group; cluster non empty finite unital Group-like associative p -commutative-group for Subgroup of G; existence ex b1 being Subgroup of G st ( b1 is p -commutative-group & b1 is finite ) proof take (1). G ; ::_thesis: ( (1). G is p -commutative-group & (1). G is finite ) ( (1). G is p -commutative-group-like & (1). G is p -group ) by Th16, Th27; hence ( (1). G is p -commutative-group & (1). G is finite ) ; ::_thesis: verum end; end; registration let p be prime Nat; let G be finite Group; let H1 be p -commutative-group-like Subgroup of G; let H2 be Subgroup of G; clusterH1 /\ H2 -> p -commutative-group-like ; coherence H1 /\ H2 is p -commutative-group-like proof reconsider H = H1 /\ H2 as Subgroup of H1 by GROUP_2:88; H is p -commutative-group-like ; hence H1 /\ H2 is p -commutative-group-like ; ::_thesis: verum end; clusterH2 /\ H1 -> p -commutative-group-like ; coherence H2 /\ H1 is p -commutative-group-like ; end; registration let p be prime Nat; let G be finite p -commutative-group-like Group; let N be normal Subgroup of G; clusterG ./. N -> p -commutative-group-like ; coherence G ./. N is p -commutative-group-like proof let S, T be Element of (G ./. N); :: according to GROUPP_1:def_3 ::_thesis: (S * T) |^ p = (S |^ p) * (T |^ p) consider a being Element of G such that A1: ( S = a * N & S = N * a ) by GROUP_6:21; consider b being Element of G such that A2: ( T = b * N & T = N * b ) by GROUP_6:21; A3: S * T = (@ S) * (@ T) by GROUP_6:19 .= (a * b) * N by A1, A2, GROUP_11:1 ; set c = a * b; A4: (S * T) |^ p = ((a * b) |^ p) * N by A3, Th8 .= ((a |^ p) * (b |^ p)) * N by Def3 .= ((a |^ p) * N) * ((b |^ p) * N) by GROUP_11:1 ; A5: S |^ p = (a |^ p) * N by A1, Th8; T |^ p = (b |^ p) * N by A2, Th8; hence (S * T) |^ p = (S |^ p) * (T |^ p) by A4, A5, GROUP_6:def_3; ::_thesis: verum end; end; theorem :: GROUPP_1:29 for p being prime Nat for G being finite Group for a, b being Element of G st G is p -commutative-group-like holds for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) proof let p be prime Nat; ::_thesis: for G being finite Group for a, b being Element of G st G is p -commutative-group-like holds for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) let G be finite Group; ::_thesis: for a, b being Element of G st G is p -commutative-group-like holds for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) let a, b be Element of G; ::_thesis: ( G is p -commutative-group-like implies for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) ) assume A1: G is p -commutative-group-like ; ::_thesis: for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) defpred S1[ Nat] means for n being Nat holds (a * b) |^ (p |^ \$1) = (a |^ (p |^ \$1)) * (b |^ (p |^ \$1)); A2: (a * b) |^ (p |^ 0) = (a * b) |^ 1 by NEWTON:4 .= a * b by GROUP_1:26 ; (a |^ (p |^ 0)) * (b |^ (p |^ 0)) = (a |^ 1) * (b |^ (p |^ 0)) by NEWTON:4 .= a * (b |^ (p |^ 0)) by GROUP_1:26 .= a * (b |^ 1) by NEWTON:4 .= a * b by GROUP_1:26 ; then A3: S1[ 0 ] by A2; A4: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A5: S1[n] ; ::_thesis: S1[n + 1] set a1 = a |^ (p |^ n); set b1 = b |^ (p |^ n); (a * b) |^ (p |^ (n + 1)) = (a * b) |^ ((p |^ n) * p) by NEWTON:6 .= ((a * b) |^ (p |^ n)) |^ p by GROUP_1:35 .= ((a |^ (p |^ n)) * (b |^ (p |^ n))) |^ p by A5 .= ((a |^ (p |^ n)) |^ p) * ((b |^ (p |^ n)) |^ p) by A1, Def3 .= (a |^ ((p |^ n) * p)) * ((b |^ (p |^ n)) |^ p) by GROUP_1:35 .= (a |^ ((p |^ n) * p)) * (b |^ ((p |^ n) * p)) by GROUP_1:35 .= (a |^ (p |^ (n + 1))) * (b |^ ((p |^ n) * p)) by NEWTON:6 .= (a |^ (p |^ (n + 1))) * (b |^ (p |^ (n + 1))) by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4); hence for n being Nat holds (a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) ; ::_thesis: verum end; theorem :: GROUPP_1:30 for p being prime Nat for G being finite commutative Group for H, H1, H2 being Subgroup of G st H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 holds H is p -commutative-group proof let p be prime Nat; ::_thesis: for G being finite commutative Group for H, H1, H2 being Subgroup of G st H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 holds H is p -commutative-group let G be finite commutative Group; ::_thesis: for H, H1, H2 being Subgroup of G st H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 holds H is p -commutative-group let H, H1, H2 be Subgroup of G; ::_thesis: ( H1 is p -commutative-group & H2 is p -commutative-group & the carrier of H = H1 * H2 implies H is p -commutative-group ) assume that A1: ( H1 is p -commutative-group & H2 is p -commutative-group ) and A2: the carrier of H = H1 * H2 ; ::_thesis: H is p -commutative-group H is p -group by A1, A2, Th19; hence H is p -commutative-group ; ::_thesis: verum end; theorem :: GROUPP_1:31 for p being prime Nat for G being finite Group for H being Subgroup of G for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) proof let p be prime Nat; ::_thesis: for G being finite Group for H being Subgroup of G for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) let G be finite Group; ::_thesis: for H being Subgroup of G for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) let H be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) let N be strict normal Subgroup of G; ::_thesis: ( N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group implies ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) ) assume that A1: N is Subgroup of center G and A2: ( H is p -commutative-group & N is p -commutative-group ) ; ::_thesis: ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) consider P being strict Subgroup of G such that A3: ( the carrier of P = H * N & P is p -group ) by A2, Th20; set P1 = P; for a, b being Element of P holds (a * b) |^ p = (a |^ p) * (b |^ p) proof let a, b be Element of P; ::_thesis: (a * b) |^ p = (a |^ p) * (b |^ p) A4: ( a in H * N & b in H * N ) by A3; then consider a1, a2 being Element of G such that A5: ( a = a1 * a2 & a1 in H & a2 in N ) by GROUP_11:6; A6: a2 in center G by A1, A5, GROUP_2:40; consider b1, b2 being Element of G such that A7: ( b = b1 * b2 & b1 in H & b2 in N ) by A4, GROUP_11:6; A8: b2 in center G by A1, A7, GROUP_2:40; then ( a2 * b2 in center G & b2 * a2 in center G ) by A6, GROUP_2:50; then A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:77; reconsider c1 = a1, d1 = b1 as Element of H by A5, A7, STRUCT_0:def_5; A10: ( a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p ) by GROUP_4:2; a1 * b1 = c1 * d1 by GROUP_2:43; then A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4 .= (c1 |^ p) * (d1 |^ p) by A2, Def3 .= (a1 |^ p) * (b1 |^ p) by A10, GROUP_2:43 ; reconsider c2 = a2, d2 = b2 as Element of N by A5, A7, STRUCT_0:def_5; A12: ( a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p ) by GROUP_4:2; b2 * a2 = d2 * c2 by GROUP_2:43; then A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4 .= (d2 |^ p) * (c2 |^ p) by A2, Def3 .= (b2 |^ p) * (a2 |^ p) by A12, GROUP_2:43 ; A14: a2 |^ p in center G by A6, GROUP_4:4; A15: a1 * a2 = a2 * a1 by A6, GROUP_5:77; A16: b1 * b2 = b2 * b1 by A8, GROUP_5:77; a * b = (a1 * a2) * (b1 * b2) by A5, A7, GROUP_2:43; then A17: (a * b) |^ p = ((a1 * a2) * (b1 * b2)) |^ p by GROUP_8:4 .= (a1 * (a2 * (b1 * b2))) |^ p by GROUP_1:def_3 .= (a1 * ((b1 * b2) * a2)) |^ p by A6, GROUP_5:77 .= (a1 * (b1 * (b2 * a2))) |^ p by GROUP_1:def_3 .= ((a1 * b1) * (b2 * a2)) |^ p by GROUP_1:def_3 .= ((a1 * b1) |^ p) * ((b2 * a2) |^ p) by A9, GROUP_1:38 .= ((a1 |^ p) * (b1 |^ p)) * ((a2 |^ p) * (b2 |^ p)) by A11, A13, A14, GROUP_5:77 .= (a1 |^ p) * ((b1 |^ p) * ((a2 |^ p) * (b2 |^ p))) by GROUP_1:def_3 .= (a1 |^ p) * (((b1 |^ p) * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def_3 .= (a1 |^ p) * (((a2 |^ p) * (b1 |^ p)) * (b2 |^ p)) by A14, GROUP_5:77 .= ((a1 |^ p) * ((a2 |^ p) * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def_3 .= (((a1 |^ p) * (a2 |^ p)) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def_3 .= ((a1 |^ p) * (a2 |^ p)) * ((b1 |^ p) * (b2 |^ p)) by GROUP_1:def_3 .= ((a1 * a2) |^ p) * ((b1 |^ p) * (b2 |^ p)) by A15, GROUP_1:38 .= ((a1 * a2) |^ p) * ((b1 * b2) |^ p) by A16, GROUP_1:38 ; A18: a |^ p = (a1 * a2) |^ p by A5, GROUP_4:2; b |^ p = (b1 * b2) |^ p by A7, GROUP_4:2; hence (a * b) |^ p = (a |^ p) * (b |^ p) by A17, A18, GROUP_2:43; ::_thesis: verum end; then P is p -commutative-group-like by Def3; hence ex P being strict Subgroup of G st ( the carrier of P = H * N & P is p -commutative-group ) by A3; ::_thesis: verum end; theorem :: GROUPP_1:32 for p being prime Nat for G being finite Group for N1, N2 being normal Subgroup of G st N2 is Subgroup of center G & N1 is p -commutative-group & N2 is p -commutative-group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) proof let p be prime Nat; ::_thesis: for G being finite Group for N1, N2 being normal Subgroup of G st N2 is Subgroup of center G & N1 is p -commutative-group & N2 is p -commutative-group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) let G be finite Group; ::_thesis: for N1, N2 being normal Subgroup of G st N2 is Subgroup of center G & N1 is p -commutative-group & N2 is p -commutative-group holds ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) let N1, N2 be normal Subgroup of G; ::_thesis: ( N2 is Subgroup of center G & N1 is p -commutative-group & N2 is p -commutative-group implies ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) ) assume that A1: N2 is Subgroup of center G and A2: ( N1 is p -commutative-group & N2 is p -commutative-group ) ; ::_thesis: ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) consider N being strict normal Subgroup of G such that A3: ( the carrier of N = N1 * N2 & N is p -group ) by A2, Th21; for a, b being Element of N holds (a * b) |^ p = (a |^ p) * (b |^ p) proof let a, b be Element of N; ::_thesis: (a * b) |^ p = (a |^ p) * (b |^ p) A4: ( a in N1 * N2 & b in N1 * N2 ) by A3; then consider a1, a2 being Element of G such that A5: ( a = a1 * a2 & a1 in N1 & a2 in N2 ) by GROUP_11:6; A6: a2 in center G by A1, A5, GROUP_2:40; consider b1, b2 being Element of G such that A7: ( b = b1 * b2 & b1 in N1 & b2 in N2 ) by A4, GROUP_11:6; A8: b2 in center G by A1, A7, GROUP_2:40; then ( a2 * b2 in center G & b2 * a2 in center G ) by A6, GROUP_2:50; then A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:77; reconsider c1 = a1, d1 = b1 as Element of N1 by A5, A7, STRUCT_0:def_5; A10: ( a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p ) by GROUP_4:2; a1 * b1 = c1 * d1 by GROUP_2:43; then A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4 .= (c1 |^ p) * (d1 |^ p) by A2, Def3 .= (a1 |^ p) * (b1 |^ p) by A10, GROUP_2:43 ; reconsider c2 = a2, d2 = b2 as Element of N2 by A5, A7, STRUCT_0:def_5; A12: ( a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p ) by GROUP_4:2; b2 * a2 = d2 * c2 by GROUP_2:43; then A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4 .= (d2 |^ p) * (c2 |^ p) by A2, Def3 .= (b2 |^ p) * (a2 |^ p) by A12, GROUP_2:43 ; A14: a2 |^ p in center G by A6, GROUP_4:4; A15: a1 * a2 = a2 * a1 by A6, GROUP_5:77; A16: b1 * b2 = b2 * b1 by A8, GROUP_5:77; a * b = (a1 * a2) * (b1 * b2) by A5, A7, GROUP_2:43; then A17: (a * b) |^ p = ((a1 * a2) * (b1 * b2)) |^ p by GROUP_8:4 .= (a1 * (a2 * (b1 * b2))) |^ p by GROUP_1:def_3 .= (a1 * ((b1 * b2) * a2)) |^ p by A6, GROUP_5:77 .= (a1 * (b1 * (b2 * a2))) |^ p by GROUP_1:def_3 .= ((a1 * b1) * (b2 * a2)) |^ p by GROUP_1:def_3 .= ((a1 * b1) |^ p) * ((b2 * a2) |^ p) by A9, GROUP_1:38 .= ((a1 |^ p) * (b1 |^ p)) * ((a2 |^ p) * (b2 |^ p)) by A11, A13, A14, GROUP_5:77 .= (a1 |^ p) * ((b1 |^ p) * ((a2 |^ p) * (b2 |^ p))) by GROUP_1:def_3 .= (a1 |^ p) * (((b1 |^ p) * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def_3 .= (a1 |^ p) * (((a2 |^ p) * (b1 |^ p)) * (b2 |^ p)) by A14, GROUP_5:77 .= ((a1 |^ p) * ((a2 |^ p) * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def_3 .= (((a1 |^ p) * (a2 |^ p)) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def_3 .= ((a1 |^ p) * (a2 |^ p)) * ((b1 |^ p) * (b2 |^ p)) by GROUP_1:def_3 .= ((a1 * a2) |^ p) * ((b1 |^ p) * (b2 |^ p)) by A15, GROUP_1:38 .= ((a1 * a2) |^ p) * ((b1 * b2) |^ p) by A16, GROUP_1:38 ; A18: a |^ p = (a1 * a2) |^ p by A5, GROUP_4:2; b |^ p = (b1 * b2) |^ p by A7, GROUP_4:2; hence (a * b) |^ p = (a |^ p) * (b |^ p) by A17, A18, GROUP_2:43; ::_thesis: verum end; then N is p -commutative-group-like by Def3; hence ex N being strict normal Subgroup of G st ( the carrier of N = N1 * N2 & N is p -commutative-group ) by A3; ::_thesis: verum end; theorem Th33: :: GROUPP_1:33 for p being prime Nat for G, H being Group st G,H are_isomorphic & G is p -commutative-group-like holds H is p -commutative-group-like proof let p be prime Nat; ::_thesis: for G, H being Group st G,H are_isomorphic & G is p -commutative-group-like holds H is p -commutative-group-like let G, H be Group; ::_thesis: ( G,H are_isomorphic & G is p -commutative-group-like implies H is p -commutative-group-like ) assume that A1: G,H are_isomorphic and A2: G is p -commutative-group-like ; ::_thesis: H is p -commutative-group-like let h1, h2 be Element of H; :: according to GROUPP_1:def_3 ::_thesis: (h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p) consider h being Homomorphism of G,H such that A3: h is bijective by A1, GROUP_6:def_11; consider a being Element of G such that A4: h . a = h1 by A3, GROUP_6:58; consider b being Element of G such that A5: h . b = h2 by A3, GROUP_6:58; h1 * h2 = h . (a * b) by A4, A5, GROUP_6:def_6; then (h1 * h2) |^ p = h . ((a * b) |^ p) by GROUP_6:37 .= h . ((a |^ p) * (b |^ p)) by A2, Def3 .= (h . (a |^ p)) * (h . (b |^ p)) by GROUP_6:def_6 .= ((h . a) |^ p) * (h . (b |^ p)) by GROUP_6:37 .= (h1 |^ p) * (h2 |^ p) by A4, A5, GROUP_6:37 ; hence (h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p) ; ::_thesis: verum end; theorem :: GROUPP_1:34 for p being prime Nat for G, H being strict Group st G,H are_isomorphic & G is p -commutative-group holds H is p -commutative-group proof let p be prime Nat; ::_thesis: for G, H being strict Group st G,H are_isomorphic & G is p -commutative-group holds H is p -commutative-group let G, H be strict Group; ::_thesis: ( G,H are_isomorphic & G is p -commutative-group implies H is p -commutative-group ) assume that A1: G,H are_isomorphic and A2: G is p -commutative-group ; ::_thesis: H is p -commutative-group A3: H is p -group by A1, A2, Th22; H is p -commutative-group-like by A1, A2, Th33; hence H is p -commutative-group by A3; ::_thesis: verum end; registration let p be prime Nat; let G be finite p -commutative-group-like Group; let H be finite Group; let g be Homomorphism of G,H; cluster Image g -> p -commutative-group-like ; coherence Image g is p -commutative-group-like proof let g1, g2 be Element of (Image g); :: according to GROUPP_1:def_3 ::_thesis: (g1 * g2) |^ p = (g1 |^ p) * (g2 |^ p) reconsider h1 = g1, h2 = g2 as Element of H by GROUP_2:42; g1 in Image g by STRUCT_0:def_5; then consider a being Element of G such that A1: g1 = g . a by GROUP_6:45; g2 in Image g by STRUCT_0:def_5; then consider b being Element of G such that A2: g2 = g . b by GROUP_6:45; g1 * g2 = h1 * h2 by GROUP_2:43 .= g . (a * b) by A1, A2, GROUP_6:def_6 ; then A3: (g1 * g2) |^ p = (g . (a * b)) |^ p by GROUP_8:4 .= g . ((a * b) |^ p) by GROUP_6:37 .= g . ((a |^ p) * (b |^ p)) by Def3 .= (g . (a |^ p)) * (g . (b |^ p)) by GROUP_6:def_6 .= ((g . a) |^ p) * (g . (b |^ p)) by GROUP_6:37 .= (h1 |^ p) * (h2 |^ p) by A1, A2, GROUP_6:37 ; ( h1 |^ p = g1 |^ p & h2 |^ p = g2 |^ p ) by GROUP_8:4; hence (g1 * g2) |^ p = (g1 |^ p) * (g2 |^ p) by A3, GROUP_2:43; ::_thesis: verum end; end; theorem :: GROUPP_1:35 for p being prime Nat for G being finite strict Group st G is p -group & expon (G,p) = 0 holds G is p -commutative-group proof let p be prime Nat; ::_thesis: for G being finite strict Group st G is p -group & expon (G,p) = 0 holds G is p -commutative-group let G be finite strict Group; ::_thesis: ( G is p -group & expon (G,p) = 0 implies G is p -commutative-group ) assume A1: ( G is p -group & expon (G,p) = 0 ) ; ::_thesis: G is p -commutative-group then G = (1). G by Th24; hence G is p -commutative-group by A1; ::_thesis: verum end; theorem :: GROUPP_1:36 for p being prime Nat for G being finite strict Group st G is p -group & expon (G,p) = 1 holds G is p -commutative-group proof let p be prime Nat; ::_thesis: for G being finite strict Group st G is p -group & expon (G,p) = 1 holds G is p -commutative-group let G be finite strict Group; ::_thesis: ( G is p -group & expon (G,p) = 1 implies G is p -commutative-group ) assume A1: ( G is p -group & expon (G,p) = 1 ) ; ::_thesis: G is p -commutative-group then G is cyclic by Th25; hence G is p -commutative-group by A1; ::_thesis: verum end;