:: by Xiquan Liang and Dailu Li

::

:: Received April 29, 2010

:: Copyright (c) 2010-2017 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 )

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 )

for n, m being Nat st n divides p |^ m holds

ex r being Nat st

( n = p |^ r & r <= m )

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 )

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

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

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

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

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;

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

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

registration
end;

registration

let p be prime Nat;

let G be Group;

let a be p -power Element of G;

coherence

a " is p -power

end;
let G be Group;

let a be p -power Element of G;

coherence

a " is p -power

proof 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

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;

coherence

a |^ b is p -power

end;
let G be Group;

let b be Element of G;

let a be p -power Element of G;

coherence

a |^ b is p -power

proof end;

registration

let p be prime Nat;

let G be commutative Group;

let a, b be p -power Element of G;

coherence

a * b is p -power

end;
let G be commutative Group;

let a, b be p -power Element of G;

coherence

a * b is p -power

proof end;

registration

let p be prime Nat;

let G be finite p -group Group;

coherence

for b_{1} being Element of G holds b_{1} is p -power

end;
let G be finite p -group Group;

coherence

for b

proof 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

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;

coherence

for b_{1} being Subgroup of G holds b_{1} is p -group

end;
let G be finite p -group Group;

coherence

for b

proof end;

registration

let p be prime Nat;

let G be Group;

existence

ex b_{1} being Subgroup of G st b_{1} is p -group

end;
let G be Group;

existence

ex b

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

coherence

G1 /\ G2 is p -group

G2 /\ G1 is p -group ;

end;
let G be finite Group;

let G1 be p -group Subgroup of G;

let G2 be Subgroup of G;

coherence

G1 /\ G2 is p -group

proof end;

coherence G2 /\ G1 is p -group ;

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

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;

coherence

G ./. N is p -group

end;
let G be finite p -group Group;

let N be normal Subgroup of G;

coherence

G ./. N is p -group

proof 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

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

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 )

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 )

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;

coherence

Image g is p -group

end;
let G be finite p -group Group;

let H be finite Group;

let g be Homomorphism of G,H;

coherence

Image g is p -group

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

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 ;

existence

ex b_{1} being Nat st card G = p |^ b_{1}
by A1;

uniqueness

for b_{1}, b_{2} being Nat st card G = p |^ b_{1} & card G = p |^ b_{2} holds

b_{1} = b_{2}

end;
let G be Group;

assume A1: G is p -group ;

existence

ex b

uniqueness

for b

b

proof 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_{3} being Nat holds

( b_{3} = expon (G,p) iff card G = p |^ b_{3} );

for p being prime Nat

for G being Group st G is p -group holds

for b

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

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)

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

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

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

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;

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

for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p);

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

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;

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

( G is p -group & G is p -commutative-group-like );

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

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;

for b_{1} being Group st b_{1} is p -commutative-group holds

( b_{1} is p -group & b_{1} is p -commutative-group-like )
;

for b_{1} being Group st b_{1} is p -group & b_{1} is p -commutative-group-like holds

b_{1} is p -commutative-group
;

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

coherence for b

( b

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

coherence for b

b

registration

let p be prime Nat;

ex b_{1} being Group st

( b_{1} is p -commutative-group & b_{1} is finite & b_{1} is cyclic & b_{1} is commutative )

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

existence ex b

( b

proof end;

registration

let p be prime Nat;

let G be finite p -commutative-group-like Group;

coherence

for b_{1} being Subgroup of G holds b_{1} is p -commutative-group-like

end;
let G be finite p -commutative-group-like Group;

coherence

for b

proof end;

registration

let p be prime Nat;

for b_{1} being Group st b_{1} is p -group & b_{1} is finite & b_{1} is commutative holds

b_{1} is p -commutative-group

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

coherence for b

b

proof end;

registration

let p be prime Nat;

let G be Group;

existence

ex b_{1} being Subgroup of G st

( b_{1} is p -commutative-group & b_{1} is finite )

end;
let G be Group;

existence

ex b

( b

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

coherence

H1 /\ H2 is p -commutative-group-like

H2 /\ H1 is p -commutative-group-like ;

end;
let G be finite Group;

let H1 be p -commutative-group-like Subgroup of G;

let H2 be Subgroup of G;

coherence

H1 /\ H2 is p -commutative-group-like

proof end;

coherence H2 /\ H1 is p -commutative-group-like ;

registration

let p be prime Nat;

let G be finite p -commutative-group-like Group;

let N be normal Subgroup of G;

coherence

G ./. N is p -commutative-group-like

end;
let G be finite p -commutative-group-like Group;

let N be normal Subgroup of G;

coherence

G ./. N is p -commutative-group-like

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

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

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 )

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 )

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

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;

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;

coherence

Image g is p -commutative-group-like

end;
let G be finite p -commutative-group-like Group;

let H be finite Group;

let g be Homomorphism of G,H;

coherence

Image g is p -commutative-group-like

proof 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

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

for G being finite strict Group st G is p -group & expon (G,p) = 1 holds

G is p -commutative-group

proof end;