:: 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;