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

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 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 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 ) by GROUP_2:108, GROUP_2:103;

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 Nat;
let G be Group;
let a be Element of G;

attr a 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 end;

registration

let G be Group;
let m be Nat;

cluster m -power for Element of the carrier of G;

existence
ex b₁ being Element of G st b₁ is m -power

proof end;

end;

registration

let p be prime Nat;
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 prime Nat st a |^ b is p -power holds
a is p -power

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

cluster a |^ b -> p -power ;

coherence
a |^ b is p -power

proof end;

end;

registration

let p be prime Nat;
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 prime Nat;
let G be finite p -group Group;

cluster -> p -power for Element of the carrier of G;

coherence
for b₁ being Element of G holds b₁ is p -power

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

registration

let p be prime Nat;
let G be finite p -group Group;

cluster -> p -group for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ is p -group

proof end;

end;

theorem Th16: :: GROUPP_1:16

for G being Group
for p being prime Nat holds (1). G is p -group

proof 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 b₁ being Subgroup of G st b₁ is p -group

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

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

registration

let p be prime Nat;
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 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 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 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 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 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 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 by GROUP_6:73;

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 b₁ being Nat st card G = p |^ b₁ by A1;
uniqueness
for b₁, b₂ being Nat st card G = p |^ b₁ & card G = p |^ b₂ holds
b₁ = b₂

proof 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 b₃ being Nat holds
( b₃ = expon (G,p) iff card G = p |^ b₃ );

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

definition

let p be Nat;
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 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;

attr G is p -commutative-group means :: GROUPP_1:def 4
( G is p -group & G is p -commutative-group-like );

end;

:: deftheorem 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 b₁ being Group st b₁ is p -commutative-group holds
( b₁ is p -group & b₁ is p -commutative-group-like ) ;

cluster non empty Group-like associative p -group p -commutative-group-like -> p -commutative-group for multMagma ;

coherence
for b₁ being Group st b₁ is p -group & b₁ is p -commutative-group-like holds
b₁ is p -commutative-group ;

end;

theorem Th27: :: GROUPP_1:27

for G being Group
for p being prime Nat holds (1). G is p -commutative-group-like

proof end;

registration

let p be prime Nat;

cluster non empty finite unital Group-like associative commutative cyclic p -commutative-group for multMagma ;

existence
ex b₁ being Group st
( b₁ is p -commutative-group & b₁ is finite & b₁ is cyclic & b₁ is commutative )

proof 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 b₁ being Subgroup of G holds b₁ is p -commutative-group-like

proof 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 b₁ being Group st b₁ is p -group & b₁ is finite & b₁ is commutative holds
b₁ is p -commutative-group

proof 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 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 b₁ being Subgroup of G st
( b₁ is p -commutative-group & b₁ is finite )

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

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 prime Nat;
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 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 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 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 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 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 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 by Th22, Th33;

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