:: by Dailu Li , Xiquan Liang and Yanhong Men

::

:: Received November 10, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th5: :: GRNILP_1:5

for G being Group

for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).]

for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).]

proof end;

theorem :: GRNILP_1:8

for G being Group

for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G

for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G

proof end;

definition

let G be Group;

let A, B be Subgroup of G;

:: original: [.

redefine func [.A,B.] -> Subgroup of G;

commutativity

for A, B being Subgroup of G holds [.A,B.] = [.B,A.]

end;
let A, B be Subgroup of G;

:: original: [.

redefine func [.A,B.] -> Subgroup of G;

commutativity

for A, B being Subgroup of G holds [.A,B.] = [.B,A.]

proof end;

theorem Th10: :: GRNILP_1:10

for G being Group

for A, B being Subgroup of G st B is Subgroup of A holds

commutators (A,B) c= carr A

for A, B being Subgroup of G st B is Subgroup of A holds

commutators (A,B) c= carr A

proof end;

Lm1: for G being Group

for A being Subgroup of G holds gr (carr A) is Subgroup of A

proof end;

theorem :: GRNILP_1:12

Lm2: for G being Group

for A being Subgroup of G holds A is Subgroup of (Omega). G

proof end;

theorem :: GRNILP_1:13

for G being Group

for H, H1, H2 being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds

[.(H1 /\ H),H.] is Subgroup of H2 /\ H

for H, H1, H2 being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds

[.(H1 /\ H),H.] is Subgroup of H2 /\ H

proof end;

Lm3: for G being Group

for H being Subgroup of G

for N being normal Subgroup of G holds [.N,H.] is Subgroup of N

proof end;

theorem Th15: :: GRNILP_1:15

for G being Group

for A being Subgroup of G holds

( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )

for A being Subgroup of G holds

( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )

proof end;

definition

let G be Group;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict normal Subgroup of G )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is strict normal Subgroup of G ) ) & ( for x being object holds

( x in b_{2} iff x is strict normal Subgroup of G ) ) holds

b_{1} = b_{2}

end;
func the_normal_subgroups_of G -> set means :Def1: :: GRNILP_1:def 1

for x being object holds

( x in it iff x is strict normal Subgroup of G );

existence for x being object holds

( x in it iff x is strict normal Subgroup of G );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def 1 :

for G being Group

for b_{2} being set holds

( b_{2} = the_normal_subgroups_of G iff for x being object holds

( x in b_{2} iff x is strict normal Subgroup of G ) );

for G being Group

for b

( b

( x in b

theorem Th16: :: GRNILP_1:16

for G being Group

for F being FinSequence of the_normal_subgroups_of G

for j being Element of NAT st j in dom F holds

F . j is strict normal Subgroup of G

for F being FinSequence of the_normal_subgroups_of G

for j being Element of NAT st j in dom F holds

F . j is strict normal Subgroup of G

proof end;

theorem Th18: :: GRNILP_1:18

for G being Group

for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G

for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G

proof end;

definition

let IT be Group;

end;
attr IT is nilpotent means :Def2: :: GRNILP_1:def 2

ex F being FinSequence of the_normal_subgroups_of IT st

( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) );

ex F being FinSequence of the_normal_subgroups_of IT st

( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) );

:: deftheorem Def2 defines nilpotent GRNILP_1:def 2 :

for IT being Group holds

( IT is nilpotent iff ex F being FinSequence of the_normal_subgroups_of IT st

( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ) );

for IT being Group holds

( IT is nilpotent iff ex F being FinSequence of the_normal_subgroups_of IT st

( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ) );

registration
end;

theorem Th19: :: GRNILP_1:19

for G being Group

for G1 being Subgroup of G

for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds

[.G1,((Omega). G).] is Subgroup of N

for G1 being Subgroup of G

for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds

[.G1,((Omega). G).] is Subgroup of N

proof end;

theorem Th20: :: GRNILP_1:20

for G being Group

for G1 being Subgroup of G

for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds

G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N)

for G1 being Subgroup of G

for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds

G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N)

proof end;

theorem Th21: :: GRNILP_1:21

for G being Group holds

( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) )

( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) )

proof end;

theorem Th22: :: GRNILP_1:22

for G being Group

for H, G1 being Subgroup of G

for G2 being strict normal Subgroup of G

for H1 being Subgroup of H

for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds

H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2)

for H, G1 being Subgroup of G

for G2 being strict normal Subgroup of G

for H1 being Subgroup of H

for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds

H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2)

proof end;

Lm4: for G being Group

for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H

proof end;

Lm5: for G being Group

for F1 being strict Subgroup of G

for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds

F1 /\ H is normal Subgroup of F2 /\ H

proof end;

registration

let G be nilpotent Group;

coherence

for b_{1} being Subgroup of G holds b_{1} is nilpotent

end;
coherence

for b

proof end;

registration

correctness

coherence

for b_{1} being Group st b_{1} is commutative holds

b_{1} is nilpotent ;

for b_{1} being Group st b_{1} is cyclic holds

b_{1} is nilpotent
;

end;
coherence

for b

b

proof end;

coherence for b

b

theorem Th23: :: GRNILP_1:23

for G, H being strict Group

for h being Homomorphism of G,H

for A being strict Subgroup of G

for a, b being Element of G holds

( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )

for h being Homomorphism of G,H

for A being strict Subgroup of G

for a, b being Element of G holds

( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )

proof end;

theorem Th24: :: GRNILP_1:24

for G, H being strict Group

for h being Homomorphism of G,H

for A being strict Subgroup of G

for a, b being Element of G

for H1 being Subgroup of Image h

for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds

(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)

for h being Homomorphism of G,H

for A being strict Subgroup of G

for a, b being Element of G

for H1 being Subgroup of Image h

for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds

(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)

proof end;

theorem Th25: :: GRNILP_1:25

for G, H being strict Group

for h being Homomorphism of G,H

for G1 being strict Subgroup of G

for G2 being strict normal Subgroup of G

for H1 being strict Subgroup of Image h

for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds

H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2)

for h being Homomorphism of G,H

for G1 being strict Subgroup of G

for G2 being strict normal Subgroup of G

for H1 being strict Subgroup of Image h

for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds

H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2)

proof end;

theorem Th26: :: GRNILP_1:26

for G, H being strict Group

for h being Homomorphism of G,H

for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h

for h being Homomorphism of G,H

for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h

proof end;

registration

let G be strict nilpotent Group;

let H be strict Group;

let h be Homomorphism of G,H;

coherence

Image h is nilpotent

end;
let H be strict Group;

let h be Homomorphism of G,H;

coherence

Image h is nilpotent

proof end;

registration

let G be strict nilpotent Group;

let N be strict normal Subgroup of G;

coherence

G ./. N is nilpotent

end;
let N be strict normal Subgroup of G;

coherence

G ./. N is nilpotent

proof end;

theorem :: GRNILP_1:27

for G being Group st ex F being FinSequence of the_normal_subgroups_of G st

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1 being strict normal Subgroup of G st G1 = F . i holds

[.G1,((Omega). G).] = F . (i + 1) ) ) holds

G is nilpotent

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1 being strict normal Subgroup of G st G1 = F . i holds

[.G1,((Omega). G).] = F . (i + 1) ) ) holds

G is nilpotent

proof end;

theorem :: GRNILP_1:28

for G being Group st ex F being FinSequence of the_normal_subgroups_of G st

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G ./. G2 is commutative Group ) ) ) holds

G is nilpotent

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G ./. G2 is commutative Group ) ) ) holds

G is nilpotent

proof end;

theorem :: GRNILP_1:29

for G being Group st ex F being FinSequence of the_normal_subgroups_of G st

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) holds

G is nilpotent

( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds

for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds

( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) holds

G is nilpotent

proof end;

registration

correctness

coherence

for b_{1} being Group st b_{1} is nilpotent holds

b_{1} is solvable ;

end;
coherence

for b

b

proof end;