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


begin

theorem Th1: :: GROUPP_1:1
for n being Nat
for p being natural prime number st ( for r being natural number holds n <> p |^ r ) holds
ex s being Element of NAT st
( s is prime & s divides n & s <> p )
proof end;

theorem Th2: :: GROUPP_1:2
for p being natural prime number
for n, m being natural number st n divides p |^ m holds
ex r being natural number st
( n = p |^ r & r <= m )
proof 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 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 end;

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

theorem Th6: :: GROUPP_1:6
for G being Group
for a, b being Element of G holds ord (a |^ b) = ord a
proof 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 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 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 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 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 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 end;

definition
let p be natural number ;
let G be Group;
let a be Element of G;
attr a is p -power means :Def1: :: GROUPP_1:def 1
 ex r being natural number st ord a = p |^ r;
end;

:: deftheorem Def1 defines -power GROUPP_1:def 1 :
for p being natural number
for G being Group
for a being Element of G holds
( a is p -power iff ex r being natural number 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 end;

registration
let G be Group;
let m be Nat;
cluster m -power Element of the carrier of G;
existence
ex b1 being Element of G st b1 is m -power
proof end;
end;

registration
let p be natural prime number ;
let G be Group;
let a be p -power Element of G;
cluster a " -> p -power ;
coherence
a " is p -power
proof end;
end;

theorem :: GROUPP_1:14
for G being Group
for a, b being Element of G
for p being natural prime number st a |^ b is p -power holds
a is p -power
proof end;

registration
let p be natural prime number ;
let G be Group;
let b be Element of G;
let a be p -power Element of G;
cluster a |^ b -> p -power ;
coherence
a |^ b is p -power
proof end;
end;

registration
let p be natural prime number ;
let G be commutative Group;
let a, b be p -power Element of G;
cluster a * b -> p -power ;
coherence
a * b is p -power
proof end;
end;

registration
let p be natural prime number ;
let G be finite p -group Group;
cluster -> p -power Element of the carrier of G;
coherence
for b1 being Element of G holds b1 is p -power
proof end;
end;

theorem Th15: :: GROUPP_1:15
for p being natural prime number
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 end;

registration
let p be natural prime number ;
let G be finite p -group Group;
cluster -> p -group Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is p -group
proof end;
end;

theorem Th16: :: GROUPP_1:16
for G being Group
for p being natural prime number holds (1). G is p -group
proof end;

registration
let p be natural prime number ;
let G be Group;
cluster non empty unital Group-like associative p -group Subgroup of G;
existence
ex b1 being Subgroup of G st b1 is p -group
proof end;
end;

registration
let p be natural prime number ;
let G be finite Group;
let G1 be p -group Subgroup of G;
let G2 be Subgroup of G;
cluster G1 /\ G2 -> p -group ;
coherence
G1 /\ G2 is p -group
proof end;
cluster G2 /\ G1 -> p -group ;
coherence
G2 /\ G1 is p -group ;
end;

theorem Th17: :: GROUPP_1:17
for p being natural prime number
for G being finite Group st ( for a being Element of G holds a is p -power ) holds
G is p -group
proof end;

registration
let p be natural prime number ;
let G be finite p -group Group;
let N be normal Subgroup of G;
cluster G ./. N -> p -group ;
coherence
G ./. N is p -group
proof end;
end;

theorem :: GROUPP_1:18
for p being natural prime number
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 end;

theorem Th19: :: GROUPP_1:19
for p being natural prime number
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 end;

theorem Th20: :: GROUPP_1:20
for p being natural prime number
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 end;

theorem Th21: :: GROUPP_1:21
for p being natural prime number
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 end;

registration
let p be natural prime number ;
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 end;
end;

theorem Th22: :: GROUPP_1:22
for p being natural prime number
for G, H being strict Group st G,H are_isomorphic & G is p -group holds
H is p -group
proof end;

definition
let p be natural prime number ;
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 end;
end;

:: deftheorem Def2 defines expon GROUPP_1:def 2 :
for p being natural prime number
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 natural prime number ;
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 13;
end;

theorem :: GROUPP_1:23
for p being natural prime number
for G being finite Group
for H being Subgroup of G st G is p -group holds
expon (H,p) <= expon (G,p)
proof end;

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

theorem Th25: :: GROUPP_1:25
for p being natural prime number
for G being finite strict Group st G is p -group & expon (G,p) = 1 holds
G is cyclic
proof end;

theorem :: GROUPP_1:26
for G being finite Group
for p being natural prime number
for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds
G is commutative
proof end;

begin

definition
let p be natural number ;
let G be Group;
attr G 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 natural number
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 natural number ;
let G be Group;
attr G 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 natural number
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 natural number ;
cluster non empty Group-like associative p -commutative-group -> p -group p -commutative-group-like 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 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 natural prime number holds (1). G is p -commutative-group-like
proof end;

registration
let p be natural prime number ;
cluster non empty finite unital Group-like associative commutative cyclic p -commutative-group multMagma ;
existence
ex b1 being Group st
( b1 is p -commutative-group & b1 is finite & b1 is cyclic & b1 is commutative )
proof end;
end;

registration
let p be natural prime number ;
let G be finite p -commutative-group-like Group;
cluster -> p -commutative-group-like Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is p -commutative-group-like
proof end;
end;

registration
let p be natural prime number ;
cluster non empty finite Group-like associative commutative p -group -> p -commutative-group multMagma ;
coherence
for b1 being Group st b1 is p -group & b1 is finite & b1 is commutative holds
b1 is p -commutative-group
proof end;
end;

theorem :: GROUPP_1:28
for p being natural prime number
for G being finite strict Group st card G = p holds
G is p -commutative-group
proof end;

registration
let p be natural prime number ;
let G be Group;
cluster non empty finite unital Group-like associative p -commutative-group Subgroup of G;
existence
ex b1 being Subgroup of G st
( b1 is p -commutative-group & b1 is finite )
proof end;
end;

registration
let p be natural prime number ;
let G be finite Group;
let H1 be p -commutative-group-like Subgroup of G;
let H2 be Subgroup of G;
cluster H1 /\ H2 -> p -commutative-group-like ;
coherence
H1 /\ H2 is p -commutative-group-like
proof end;
cluster H2 /\ H1 -> p -commutative-group-like ;
coherence
H2 /\ H1 is p -commutative-group-like ;
end;

registration
let p be natural prime number ;
let G be finite p -commutative-group-like Group;
let N be normal Subgroup of G;
cluster G ./. N -> p -commutative-group-like ;
coherence
G ./. N is p -commutative-group-like
proof end;
end;

theorem :: GROUPP_1:29
for p being natural prime number
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 end;

theorem :: GROUPP_1:30
for p being natural prime number
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 end;

theorem :: GROUPP_1:31
for p being natural prime number
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 end;

theorem :: GROUPP_1:32
for p being natural prime number
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 end;

theorem Th33: :: GROUPP_1:33
for p being natural prime number
for G, H being Group st G,H are_isomorphic & G is p -commutative-group-like holds
H is p -commutative-group-like
proof end;

theorem :: GROUPP_1:34
for p being natural prime number
for G, H being strict Group st G,H are_isomorphic & G is p -commutative-group holds
H is p -commutative-group
proof end;

registration
let p be natural prime number ;
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 end;
end;

theorem :: GROUPP_1:35
for p being natural prime number
for G being finite strict Group st G is p -group & expon (G,p) = 0 holds
G is p -commutative-group
proof end;

theorem :: GROUPP_1:36
for p being natural prime number
for G being finite strict Group st G is p -group & expon (G,p) = 1 holds
G is p -commutative-group
proof end;