:: Some Properties of $p$-Groups and Commutative $p$-Groups
:: by Xiquan Liang and Dailu Li
::
:: Received April 29, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


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 &amp; s divides n &amp; s <> p )
proofend;

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 &amp; r <= m )
proofend;

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

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

theorem Th5: :: GROUPP_1:5
for G being Group
for a being Element of G holds ord (a ") = ord a
proofend;

theorem Th6: :: GROUPP_1:6
for G being Group
for a, b being Element of G holds ord (a |^ b) = ord a
proofend;

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 &amp; b in N holds
for n being Nat ex g being Element of G st
( g in N &amp; (a * b) |^ n = (a |^ n) * g )
proofend;

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

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 &amp; h in H )
proofend;

theorem Th10: :: GROUPP_1:10
for G being finite Group
for N being normal Subgroup of G st N is Subgroup of center G &amp; G ./. N is cyclic holds
G is commutative
proofend;

theorem :: GROUPP_1:11
for G being finite Group
for N being normal Subgroup of G st N = center G &amp; G ./. N is cyclic holds
G is commutative
proofend;

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

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

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

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
proofend;
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
proofend;
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
proofend;
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 &amp; a in H holds
a is p -power
proofend;

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
proofend;
end;

theorem Th16: :: GROUPP_1:16
for G being Group
for p being prime Nat holds (1). G is p -group
proofend;

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

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
proofend;
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 &amp; G ./. N is p -group holds
G is p -group
proofend;

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 &amp; H2 is p -group &amp; the carrier of H = H1 * H2 holds
H is p -group
proofend;

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 &amp; H is p -group &amp; N is p -group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N &amp; P is p -group )
proofend;

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 &amp; N2 is p -group holds
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 &amp; N is p -group )
proofend;

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
proofend;
end;

theorem Th22: :: GROUPP_1:22
for p being prime Nat
for G, H being strict Group st G,H are_isomorphic &amp; G is p -group holds
H is p -group
proofend;

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 &amp; card G = p |^ b2 holds
b1 = b2
proofend;
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)
proofend;

theorem Th24: :: GROUPP_1:24
for p being prime Nat
for G being finite strict Group st G is p -group &amp; expon (G,p) = 0 holds
G = (1). G
proofend;

theorem Th25: :: GROUPP_1:25
for p being prime Nat
for G being finite strict Group st G is p -group &amp; expon (G,p) = 1 holds
G is cyclic
proofend;

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 &amp; expon (G,p) = 2 &amp; ord a = p |^ 2 holds
G is commutative
proofend;

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 &amp; 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 &amp; 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 &amp; 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 &amp; 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
proofend;

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 &amp; b1 is finite &amp; b1 is cyclic &amp; b1 is commutative )
proofend;
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
proofend;
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 &amp; b1 is finite &amp; b1 is commutative holds
b1 is p -commutative-group
proofend;
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
proofend;

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 &amp; b1 is finite )
proofend;
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
proofend;
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
proofend;
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))
proofend;

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 &amp; H2 is p -commutative-group &amp; the carrier of H = H1 * H2 holds
H is p -commutative-group
proofend;

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 &amp; H is p -commutative-group &amp; N is p -commutative-group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N &amp; P is p -commutative-group )
proofend;

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 &amp; N1 is p -commutative-group &amp; N2 is p -commutative-group holds
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 &amp; N is p -commutative-group )
proofend;

theorem Th33: :: GROUPP_1:33
for p being prime Nat
for G, H being Group st G,H are_isomorphic &amp; G is p -commutative-group-like holds
H is p -commutative-group-like
proofend;

theorem :: GROUPP_1:34
for p being prime Nat
for G, H being strict Group st G,H are_isomorphic &amp; G is p -commutative-group holds
H is p -commutative-group
proofend;

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
proofend;
end;

theorem :: GROUPP_1:35
for p being prime Nat
for G being finite strict Group st G is p -group &amp; expon (G,p) = 0 holds
G is p -commutative-group
proofend;

theorem :: GROUPP_1:36
for p being prime Nat
for G being finite strict Group st G is p -group &amp; expon (G,p) = 1 holds
G is p -commutative-group
proofend;