:: GRNILP_1 semantic presentation
begin
theorem :: GRNILP_1:1
for G being Group
for a, b being Element of G holds a |^ b = a * [.a,b.]
proof
let G be Group; ::_thesis: for a, b being Element of G holds a |^ b = a * [.a,b.]
let a, b be Element of G; ::_thesis: a |^ b = a * [.a,b.]
a * [.a,b.] = a * (((a ") * (b ")) * (a * b)) by GROUP_1:def_3
.= a * ((a ") * ((b ") * (a * b))) by GROUP_1:def_3
.= (a * (a ")) * ((b ") * (a * b)) by GROUP_1:def_3
.= (1_ G) * ((b ") * (a * b)) by GROUP_1:def_5
.= (b ") * (a * b) by GROUP_1:def_4
.= ((b ") * a) * b by GROUP_1:def_3 ;
hence a |^ b = a * [.a,b.] ; ::_thesis: verum
end;
theorem :: GRNILP_1:2
for G being Group
for a, b being Element of G holds [.a,b.] " = [.a,(b ").] |^ b
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] " = [.a,(b ").] |^ b
let a, b be Element of G; ::_thesis: [.a,b.] " = [.a,(b ").] |^ b
thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by GROUP_1:def_3
.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17
.= (b ") * ((a ") * (b * a)) by GROUP_1:def_3
.= (b ") * (((a ") * b) * a) by GROUP_1:def_3
.= ((b ") * (((a ") * b) * a)) * (1_ G) by GROUP_1:def_4
.= ((b ") * (((a ") * b) * a)) * ((b ") * b) by GROUP_1:def_5
.= (((b ") * (((a ") * b) * a)) * (b ")) * b by GROUP_1:def_3
.= [.a,(b ").] |^ b by GROUP_1:def_3 ; ::_thesis: verum
end;
theorem :: GRNILP_1:3
for G being Group
for a, b being Element of G holds [.a,b.] " = [.(a "),b.] |^ a
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] " = [.(a "),b.] |^ a
let a, b be Element of G; ::_thesis: [.a,b.] " = [.(a "),b.] |^ a
thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by GROUP_1:def_3
.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17
.= (b ") * ((a ") * (b * a)) by GROUP_1:def_3
.= (b ") * (((a ") * b) * a) by GROUP_1:def_3
.= (1_ G) * ((b ") * (((a ") * b) * a)) by GROUP_1:def_4
.= ((a ") * a) * ((b ") * (((a ") * b) * a)) by GROUP_1:def_5
.= (a ") * (a * ((b ") * (((a ") * b) * a))) by GROUP_1:def_3
.= (a ") * ((a * (b ")) * (((a ") * b) * a)) by GROUP_1:def_3
.= (a ") * (((a * (b ")) * ((a ") * b)) * a) by GROUP_1:def_3
.= ((a ") * ((a * (b ")) * ((a ") * b))) * a by GROUP_1:def_3
.= [.(a "),b.] |^ a by GROUP_5:16 ; ::_thesis: verum
end;
theorem Th4: :: GRNILP_1:4
for G being Group
for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
proof
let G be Group; ::_thesis: for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
let a, b be Element of G; ::_thesis: ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
thus ([.a,(b ").] |^ b) " = ([.a,(b ").] ") |^ b by GROUP_3:26
.= [.(b "),a.] |^ b by GROUP_5:22 ; ::_thesis: verum
end;
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).]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).]
let a, b, c be Element of G; ::_thesis: [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).]
A1: [.a,(b "),c.] |^ b = ((b ") * ((((([.a,(b ").] ") * (1_ G)) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_4
.= ((b ") * ((((([.a,(b ").] ") * (b * (b "))) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_5
.= ((b ") * (((((([.a,(b ").] ") * b) * (b ")) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_3
.= ((b ") * ((((([.a,(b ").] ") * b) * (b ")) * (c ")) * ([.a,(b ").] * c))) * b by GROUP_1:def_3
.= ((b ") * (((([.a,(b ").] ") * b) * (b ")) * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3
.= ((b ") * ((([.a,(b ").] ") * b) * ((b ") * ((c ") * ([.a,(b ").] * c))))) * b by GROUP_1:def_3
.= (((b ") * (([.a,(b ").] ") * b)) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3
.= ((([.a,(b ").] ") |^ b) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3
.= (([.a,(b ").] ") |^ b) * (((b ") * ((c ") * ([.a,(b ").] * c))) * b) by GROUP_1:def_3
.= (([.a,(b ").] ") |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_5:22
.= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_3:24 ;
[.([.a,(b ").] |^ b),(c |^ b).] = ((([.(b "),a.] |^ b) * ((c |^ b) ")) * ([.a,(b ").] |^ b)) * (c |^ b) by Th4
.= ((([.(b "),a.] |^ b) * ((c ") |^ b)) * ([.a,(b ").] |^ b)) * (c |^ b) by GROUP_3:26
.= ((([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * b)) * ((b ") * (c * b)) by GROUP_1:def_3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * ((((b ") * [.a,(b ").]) * b) * ((b ") * (c * b))) by GROUP_1:def_3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * (b * ((b ") * (c * b)))) by GROUP_1:def_3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((b * (b ")) * (c * b))) by GROUP_1:def_3
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((1_ G) * (c * b))) by GROUP_1:def_5
.= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * (c * b)) by GROUP_1:def_4
.= ([.(b "),a.] |^ b) * ((((b ") * (c ")) * b) * (((b ") * [.a,(b ").]) * (c * b))) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (b * (((b ") * [.a,(b ").]) * (c * b)))) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * ((b * ((b ") * [.a,(b ").])) * (c * b))) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((b * (b ")) * [.a,(b ").]) * (c * b))) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((1_ G) * [.a,(b ").]) * (c * b))) by GROUP_1:def_5
.= ([.(b "),a.] |^ b) * (((b ") * (c ")) * ([.a,(b ").] * (c * b))) by GROUP_1:def_4
.= ([.(b "),a.] |^ b) * ((((b ") * (c ")) * [.a,(b ").]) * (c * b)) by GROUP_1:def_3
.= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_1:17 ;
hence [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by A1; ::_thesis: verum
end;
theorem Th6: :: GRNILP_1:6
for G being Group
for a, b being Element of G holds [.a,(b ").] |^ b = [.b,a.]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,(b ").] |^ b = [.b,a.]
let a, b be Element of G; ::_thesis: [.a,(b ").] |^ b = [.b,a.]
thus [.a,(b ").] |^ b = (b ") * (((((a ") * ((b ") ")) * a) * (b ")) * b) by GROUP_1:def_3
.= (b ") * ((((a ") * ((b ") ")) * a) * ((b ") * b)) by GROUP_1:def_3
.= (b ") * ((((a ") * ((b ") ")) * a) * (1_ G)) by GROUP_1:def_5
.= (b ") * (((a ") * ((b ") ")) * a) by GROUP_1:def_4
.= (b ") * ((a ") * (b * a)) by GROUP_1:def_3
.= ((b ") * (a ")) * (b * a) by GROUP_1:def_3
.= (((b ") * (a ")) * b) * a by GROUP_1:def_3
.= [.b,a.] ; ::_thesis: verum
end;
theorem Th7: :: GRNILP_1:7
for G being Group
for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
let a, b, c be Element of G; ::_thesis: [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
[.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by Th5;
hence [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] by Th6; ::_thesis: verum
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
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G
let a, b, c be Element of G; ::_thesis: ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G
( [.a,b,(c |^ a).] = [.b,(a "),c.] |^ a & [.c,a,(b |^ c).] = [.a,(c "),b.] |^ c & [.b,c,(a |^ b).] = [.c,(b "),a.] |^ b ) by Th7;
hence ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G by GROUP_5:46; ::_thesis: verum
end;
theorem Th9: :: GRNILP_1:9
for G being Group
for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.]
proof
let G be Group; ::_thesis: for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.]
let A, B be Subgroup of G; ::_thesis: [.A,B.] is Subgroup of [.B,A.]
now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.A,B.]_holds_
a_in_[.B,A.]
let a be Element of G; ::_thesis: ( a in [.A,B.] implies a in [.B,A.] )
assume a in [.A,B.] ; ::_thesis: a in [.B,A.]
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
len F = len I and
A1: rng F c= commutators (A,B) and
A2: a = Product (F |^ I) by GROUP_5:61;
deffunc H1( Nat) -> Element of the carrier of G = (F /. $1) " ;
consider F1 being FinSequence of the carrier of G such that
A3: len F1 = len F and
A4: for k being Nat st k in dom F1 holds
F1 . k = H1(k) from FINSEQ_2:sch_1();
A5: dom F1 = Seg (len F) by A3, FINSEQ_1:def_3;
deffunc H2( Nat) -> Element of INT = @ (- (@ (I /. $1)));
consider I1 being FinSequence of INT such that
A6: len I1 = len F and
A7: for k being Nat st k in dom I1 holds
I1 . k = H2(k) from FINSEQ_2:sch_1();
A8: dom F = Seg (len F) by FINSEQ_1:def_3;
A9: dom F1 = dom F by A3, FINSEQ_3:29;
A10: dom I1 = dom F by A6, FINSEQ_3:29;
set J = F1 |^ I1;
A11: ( len (F1 |^ I1) = len F & len (F |^ I) = len F ) by A3, GROUP_4:def_3;
then A12: dom (F |^ I) = Seg (len F) by FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(F_|^_I)_holds_
(F_|^_I)_._k_=_(F1_|^_I1)_._k
let k be Nat; ::_thesis: ( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )
assume A13: k in dom (F |^ I) ; ::_thesis: (F |^ I) . k = (F1 |^ I1) . k
then A14: k in dom F by A12, FINSEQ_1:def_3;
( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k & F1 . k = (F /. k) " & I1 . k = I1 /. k & @ (I1 /. k) = I1 /. k & I1 . k = @ (- (@ (I /. k))) & @ (- (@ (I /. k))) = - (@ (I /. k)) ) by A4, A7, A8, A9, A10, A13, A12, GROUP_4:def_3, PARTFUN1:def_6;
then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by GROUP_1:36
.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by A14, GROUP_4:def_3; ::_thesis: verum
end;
then A15: F1 |^ I1 = F |^ I by A11, FINSEQ_2:9;
rng F1 c= commutators (B,A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F1 or x in commutators (B,A) )
assume x in rng F1 ; ::_thesis: x in commutators (B,A)
then consider y being set such that
A16: y in dom F1 and
A17: F1 . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A16;
y in dom F by A3, A16, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def_3;
then consider b, c being Element of G such that
A18: F . y = [.b,c.] and
A19: ( b in A & c in B ) by A1, GROUP_5:52;
( x = (F /. y) " & F /. y = F . y ) by A16, A4, A8, A17, A5, PARTFUN1:def_6;
then x = [.c,b.] by A18, GROUP_5:22;
hence x in commutators (B,A) by A19, GROUP_5:52; ::_thesis: verum
end;
hence a in [.B,A.] by A2, A3, A6, A15, GROUP_5:61; ::_thesis: verum
end;
hence [.A,B.] is Subgroup of [.B,A.] by GROUP_2:58; ::_thesis: verum
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.]
proof
let A, B be Subgroup of G; ::_thesis: [.A,B.] = [.B,A.]
( [.A,B.] is Subgroup of [.B,A.] & [.B,A.] is Subgroup of [.A,B.] ) by Th9;
hence [.A,B.] = [.B,A.] by GROUP_2:55; ::_thesis: verum
end;
end;
theorem Th10: :: GRNILP_1:10
for G being Group
for B, A being Subgroup of G st B is Subgroup of A holds
commutators (A,B) c= carr A
proof
let G be Group; ::_thesis: for B, A being Subgroup of G st B is Subgroup of A holds
commutators (A,B) c= carr A
let B, A be Subgroup of G; ::_thesis: ( B is Subgroup of A implies commutators (A,B) c= carr A )
assume A1: B is Subgroup of A ; ::_thesis: commutators (A,B) c= carr A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (A,B) or x in carr A )
assume x in commutators (A,B) ; ::_thesis: x in carr A
then consider a, b being Element of G such that
A2: ( x = [.a,b.] & a in A & b in B ) by GROUP_5:52;
A3: b in A by A1, A2, GROUP_2:40;
then A4: a * b in A by A2, GROUP_2:50;
( a " in A & b " in A ) by A2, A3, GROUP_2:51;
then (a ") * (b ") in A by GROUP_2:50;
then A5: ((a ") * (b ")) * (a * b) in A by A4, GROUP_2:50;
[.a,b.] = ((a ") * (b ")) * (a * b) by GROUP_1:def_3;
hence x in carr A by A2, A5, STRUCT_0:def_5; ::_thesis: verum
end;
Lm1: for G being Group
for A being Subgroup of G holds gr (carr A) is Subgroup of A
proof
let G be Group; ::_thesis: for A being Subgroup of G holds gr (carr A) is Subgroup of A
let A be Subgroup of G; ::_thesis: gr (carr A) is Subgroup of A
set A9 = multMagma(# the carrier of A, the multF of A #);
( the carrier of multMagma(# the carrier of A, the multF of A #) c= the carrier of G & the multF of multMagma(# the carrier of A, the multF of A #) = the multF of G || the carrier of A ) by GROUP_2:def_5;
then reconsider A9 = multMagma(# the carrier of A, the multF of A #) as strict Subgroup of G by GROUP_2:def_5;
A1: gr (carr A) is Subgroup of A9 by GROUP_4:def_4;
A9 is Subgroup of A by GROUP_2:57;
hence gr (carr A) is Subgroup of A by A1, GROUP_2:56; ::_thesis: verum
end;
theorem Th11: :: GRNILP_1:11
for G being Group
for B, A being Subgroup of G st B is Subgroup of A holds
[.A,B.] is Subgroup of A
proof
let G be Group; ::_thesis: for B, A being Subgroup of G st B is Subgroup of A holds
[.A,B.] is Subgroup of A
let B, A be Subgroup of G; ::_thesis: ( B is Subgroup of A implies [.A,B.] is Subgroup of A )
A1: gr (carr A) is Subgroup of A by Lm1;
assume B is Subgroup of A ; ::_thesis: [.A,B.] is Subgroup of A
then commutators (A,B) c= carr A by Th10;
then [.A,B.] is Subgroup of gr (carr A) by GROUP_4:32;
hence [.A,B.] is Subgroup of A by A1, GROUP_2:56; ::_thesis: verum
end;
theorem :: GRNILP_1:12
for G being Group
for B, A being Subgroup of G st B is Subgroup of A holds
[.B,A.] is Subgroup of A by Th11;
Lm2: for G being Group
for A being Subgroup of G holds A is Subgroup of (Omega). G
proof
let G be Group; ::_thesis: for A being Subgroup of G holds A is Subgroup of (Omega). G
let A be Subgroup of G; ::_thesis: A is Subgroup of (Omega). G
dom the multF of G c= [: the carrier of G, the carrier of G:] ;
then the multF of G = the multF of ((Omega). G) || the carrier of ((Omega). G) by RELAT_1:68;
then G is Subgroup of (Omega). G by GROUP_2:def_5;
hence A is Subgroup of (Omega). G by GROUP_2:56; ::_thesis: verum
end;
theorem :: GRNILP_1:13
for G being Group
for H1, H2, H being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds
[.(H1 /\ H),H.] is Subgroup of H2 /\ H
proof
let G be Group; ::_thesis: for H1, H2, H being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds
[.(H1 /\ H),H.] is Subgroup of H2 /\ H
let H1, H2, H be Subgroup of G; ::_thesis: ( [.H1,((Omega). G).] is Subgroup of H2 implies [.(H1 /\ H),H.] is Subgroup of H2 /\ H )
assume A1: [.H1,((Omega). G).] is Subgroup of H2 ; ::_thesis: [.(H1 /\ H),H.] is Subgroup of H2 /\ H
H1 /\ H is Subgroup of H by GROUP_2:88;
then A2: [.(H1 /\ H),H.] is Subgroup of H by Th11;
A3: H is Subgroup of (Omega). G by Lm2;
H1 /\ H is Subgroup of H1 by GROUP_2:88;
then [.(H1 /\ H),H.] is Subgroup of [.H1,((Omega). G).] by A3, GROUP_5:66;
then [.(H1 /\ H),H.] is Subgroup of H2 by A1, GROUP_2:56;
hence [.(H1 /\ H),H.] is Subgroup of H2 /\ H by A2, GROUP_2:91; ::_thesis: verum
end;
theorem :: GRNILP_1:14
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
let H1, H2 be Subgroup of G; ::_thesis: [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
A1: H2 is Subgroup of (Omega). G by Lm2;
H1 is Subgroup of H1 by GROUP_2:54;
hence [.H1,H2.] is Subgroup of [.H1,((Omega). G).] by A1, GROUP_5:66; ::_thesis: verum
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
let G be Group; ::_thesis: for H being Subgroup of G
for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
let H be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
let N be normal Subgroup of G; ::_thesis: [.N,H.] is Subgroup of N
( the carrier of N c= the carrier of G & the multF of N = the multF of G || the carrier of N ) by GROUP_2:def_5;
then reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by GROUP_2:def_5;
now__::_thesis:_for_a_being_Element_of_G_holds_N9_|^_a_=_multMagma(#_the_carrier_of_N9,_the_multF_of_N9_#)
let a be Element of G; ::_thesis: N9 |^ a = multMagma(# the carrier of N9, the multF of N9 #)
the carrier of (N |^ a) = (carr N) |^ a by GROUP_3:def_6
.= (carr N9) |^ a
.= the carrier of (N9 |^ a) by GROUP_3:def_6 ;
hence N9 |^ a = N |^ a by GROUP_2:59
.= multMagma(# the carrier of N9, the multF of N9 #) by GROUP_3:def_13 ;
::_thesis: verum
end;
then reconsider N9 = N9 as strict normal Subgroup of G by GROUP_3:def_13;
[.N9,H.] = [.N,H.] ;
then A1: [.N,H.] is Subgroup of N9 by GROUP_5:67;
N9 is Subgroup of N by GROUP_2:57;
hence [.N,H.] is Subgroup of N by A1, GROUP_2:56; ::_thesis: verum
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 )
proof
let G be Group; ::_thesis: for A being Subgroup of G holds
( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )
let A be Subgroup of G; ::_thesis: ( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )
thus ( A is normal Subgroup of G implies [.A,((Omega). G).] is Subgroup of A ) by Lm3; ::_thesis: ( [.A,((Omega). G).] is Subgroup of A implies A is normal Subgroup of G )
assume A1: [.A,((Omega). G).] is Subgroup of A ; ::_thesis: A is normal Subgroup of G
for b being Element of G holds b * A c= A * b
proof
let b be Element of G; ::_thesis: b * A c= A * b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * A or x in A * b )
assume A2: x in b * A ; ::_thesis: x in A * b
then reconsider x = x as Element of G ;
consider Z being Element of G such that
A3: ( x = b * Z & Z in A ) by A2, GROUP_2:103;
A4: Z " in A by A3, GROUP_2:51;
b " in (Omega). G by STRUCT_0:def_5;
then [.(b "),(Z ").] in [.((Omega). G),A.] by A4, GROUP_5:65;
then [.(b "),(Z ").] in A by A1, GROUP_2:40;
then A5: (((b * Z) * (b ")) * (Z ")) * Z in A by A3, GROUP_2:50;
A6: (((b * Z) * (b ")) * (Z ")) * Z = ((b * Z) * (b ")) * ((Z ") * Z) by GROUP_1:def_3
.= ((b * Z) * (b ")) * (1_ G) by GROUP_1:def_5
.= (b * Z) * (b ") by GROUP_1:def_4 ;
((b * Z) * (b ")) * b = (b * Z) * ((b ") * b) by GROUP_1:def_3
.= (b * Z) * (1_ G) by GROUP_1:def_5
.= b * Z by GROUP_1:def_4 ;
hence x in A * b by A3, A5, A6, GROUP_2:104; ::_thesis: verum
end;
hence A is normal Subgroup of G by GROUP_3:118; ::_thesis: verum
end;
definition
let G be Group;
func the_normal_subgroups_of G -> set means :Def1: :: GRNILP_1:def 1
for x being set holds
( x in it iff x is strict normal Subgroup of G );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict normal Subgroup of G )
proof
defpred S1[ set , set ] means ex H being strict normal Subgroup of G st
( $2 = H & $1 = the carrier of H );
defpred S2[ set ] means ex H being strict normal Subgroup of G st $1 = the carrier of H;
consider B being set such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of G & S2[x] ) ) from XBOOLE_0:sch_1();
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by GROUP_2:59;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
for x being set holds
( x in B iff ex y being set st [x,y] in f )
proof
let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f )
thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B )
proof
assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f
then consider H being strict normal Subgroup of G such that
A5: x = the carrier of H by A1;
reconsider y = H as set ;
take y ; ::_thesis: [x,y] in f
thus [x,y] in f by A3, A4, A5; ::_thesis: verum
end;
given y being set such that A6: [x,y] in f ; ::_thesis: x in B
thus x in B by A3, A6; ::_thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def_12;
for y being set holds
( y in rng f iff y is strict normal Subgroup of G )
proof
let y be set ; ::_thesis: ( y in rng f iff y is strict normal Subgroup of G )
thus ( y in rng f implies y is strict normal Subgroup of G ) ::_thesis: ( y is strict normal Subgroup of G implies y in rng f )
proof
assume y in rng f ; ::_thesis: y is strict normal Subgroup of G
then consider x being set such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
[x,y] in f by A8, FUNCT_1:def_2;
then ex H being strict normal Subgroup of G st
( y = H & x = the carrier of H ) by A3;
hence y is strict normal Subgroup of G ; ::_thesis: verum
end;
assume y is strict normal Subgroup of G ; ::_thesis: y in rng f
then reconsider H = y as strict normal Subgroup of G ;
reconsider x = the carrier of H as set ;
the carrier of H c= the carrier of G by GROUP_2:def_5;
then A9: x in dom f by A1, A7;
then [x,y] in f by A3, A7;
then y = f . x by A9, FUNCT_1:def_2;
hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum
end;
hence ex b1 being set st
for x being set holds
( x in b1 iff x is strict normal Subgroup of G ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict normal Subgroup of G ) ) & ( for x being set holds
( x in b2 iff x is strict normal Subgroup of G ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is strict normal Subgroup of G;
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff x is strict normal Subgroup of G ) ) & ( for x being set holds
( x in A2 iff x is strict normal Subgroup of G ) ) implies A1 = A2 )
assume A10: for x being set holds
( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st
( ( x in A2 implies x is strict normal Subgroup of G ) implies ( x is strict normal Subgroup of G & not x in A2 ) ) or A1 = A2 )
assume A11: for x being set holds
( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2
thus A1 = A2 from XBOOLE_0:sch_2(A10, A11); ::_thesis: verum
end;
end;
:: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def_1_:_
for G being Group
for b2 being set holds
( b2 = the_normal_subgroups_of G iff for x being set holds
( x in b2 iff x is strict normal Subgroup of G ) );
registration
let G be Group;
cluster the_normal_subgroups_of G -> non empty ;
coherence
not the_normal_subgroups_of G is empty
proof
the strict normal Subgroup of G in the_normal_subgroups_of G by Def1;
hence not the_normal_subgroups_of G is empty ; ::_thesis: verum
end;
end;
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
proof
let G be Group; ::_thesis: 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
let F be FinSequence of the_normal_subgroups_of G; ::_thesis: for j being Element of NAT st j in dom F holds
F . j is strict normal Subgroup of G
let j be Element of NAT ; ::_thesis: ( j in dom F implies F . j is strict normal Subgroup of G )
assume j in dom F ; ::_thesis: F . j is strict normal Subgroup of G
then F . j in rng F by FUNCT_1:3;
hence F . j is strict normal Subgroup of G by Def1; ::_thesis: verum
end;
theorem Th17: :: GRNILP_1:17
for G being Group holds the_normal_subgroups_of G c= Subgroups G
proof
let G be Group; ::_thesis: the_normal_subgroups_of G c= Subgroups G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_normal_subgroups_of G or x in Subgroups G )
assume x in the_normal_subgroups_of G ; ::_thesis: x in Subgroups G
then x is strict normal Subgroup of G by Def1;
hence x in Subgroups G by GROUP_3:def_1; ::_thesis: verum
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
proof
let G be Group; ::_thesis: for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G
let F be FinSequence of the_normal_subgroups_of G; ::_thesis: F is FinSequence of Subgroups G
the_normal_subgroups_of G c= Subgroups G by Th17;
then rng F c= Subgroups G by XBOOLE_1:1;
hence F is FinSequence of Subgroups G by FINSEQ_1:def_4; ::_thesis: verum
end;
definition
let IT be Group;
attrIT 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) ) ) );
end;
:: 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) ) ) ) );
registration
cluster non empty strict unital Group-like associative nilpotent for multMagma ;
existence
ex b1 being Group st
( b1 is nilpotent & b1 is strict )
proof
set G = the Group;
take H = (1). the Group; ::_thesis: ( H is nilpotent & H is strict )
thus H is nilpotent ::_thesis: H is strict
proof
rng <*H*> c= the_normal_subgroups_of H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng <*H*> or x in the_normal_subgroups_of H )
assume A1: x in rng <*H*> ; ::_thesis: x in the_normal_subgroups_of H
rng <*H*> = {H} by FINSEQ_1:39;
then x = H by A1, TARSKI:def_1;
then x is strict normal Subgroup of H by GROUP_2:54, GROUP_6:8;
hence x in the_normal_subgroups_of H by Def1; ::_thesis: verum
end;
then reconsider F = <*H*> as FinSequence of the_normal_subgroups_of H by FINSEQ_1:def_4;
take F ; :: according to GRNILP_1:def_2 ::_thesis: ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( 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 H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) )
A2: len F = 1 by FINSEQ_1:39;
then A3: F . (len F) = H by FINSEQ_1:40
.= (1). H by GROUP_2:63 ;
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 H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )
let G1, G2 be strict normal Subgroup of H; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) )
assume ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) )
dom F = {1} by A2, FINSEQ_1:2, FINSEQ_1:def_3;
then ( i = 1 & i + 1 = 1 ) by A4, TARSKI:def_1;
hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ; ::_thesis: verum
end;
hence ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( 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 H st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) by A3, FINSEQ_1:40; ::_thesis: verum
end;
thus H is strict ; ::_thesis: verum
end;
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
proof
let G be Group; ::_thesis: 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
let G1 be Subgroup of G; ::_thesis: 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
let N be strict normal Subgroup of G; ::_thesis: ( N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) implies [.G1,((Omega). G).] is Subgroup of N )
assume that
A1: N is Subgroup of G1 and
A2: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ; ::_thesis: [.G1,((Omega). G).] is Subgroup of N
A3: (G1,N) `*` = N by A1, GROUP_6:def_1;
reconsider J = G1 ./. ((G1,N) `*`) as Subgroup of G ./. N by A1, GROUP_6:28;
reconsider I = N as normal Subgroup of G1 by A3;
A4: commutators (G1,((Omega). G)) c= carr N
proof
now__::_thesis:_for_x_being_Element_of_G_st_x_in_commutators_(G1,((Omega)._G))_holds_
x_in_carr_N
let x be Element of G; ::_thesis: ( x in commutators (G1,((Omega). G)) implies x in carr N )
assume x in commutators (G1,((Omega). G)) ; ::_thesis: x in carr N
then consider a, b being Element of G such that
A5: ( x = [.a,b.] & a in G1 & b in (Omega). G ) by GROUP_5:52;
reconsider c = a as Element of G1 by A5, STRUCT_0:def_5;
reconsider S9 = c * I as Element of J by A3, GROUP_6:22;
A6: S9 in J by STRUCT_0:def_5;
reconsider T = b * N as Element of (G ./. N) by GROUP_6:14;
reconsider d = c as Element of G ;
d * N = c * I by GROUP_6:2;
then reconsider S = S9 as Element of (G ./. N) by GROUP_6:14;
S in center (G ./. N) by A2, A6, GROUP_2:40;
then A7: S * T = T * S by GROUP_5:77;
A8: ( S = d * N & T = b * N & @ S = S & @ T = T ) by GROUP_6:2;
then A9: S * T = (d * N) * (b * N) by GROUP_6:def_3
.= d * (N * (b * N)) by GROUP_3:10
.= d * ((N * b) * N) by GROUP_3:13
.= d * ((b * N) * N) by GROUP_3:117
.= d * (b * N) by GROUP_6:5
.= (d * b) * N by GROUP_2:105 ;
T * S = (b * N) * (d * N) by A8, GROUP_6:def_3
.= b * (N * (d * N)) by GROUP_3:10
.= b * ((N * d) * N) by GROUP_3:13
.= b * ((d * N) * N) by GROUP_3:117
.= b * (d * N) by GROUP_6:5
.= (b * d) * N by GROUP_2:105 ;
then A10: ((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (b * d)) * N by A7, A9, GROUP_2:105
.= ((d ") * ((b ") * (b * d))) * N by GROUP_1:def_3
.= ((d ") * (((b ") * b) * d)) * N by GROUP_1:def_3
.= ((d ") * ((1_ G) * d)) * N by GROUP_1:def_5
.= ((d ") * d) * N by GROUP_1:def_4
.= (1_ G) * N by GROUP_1:def_5
.= carr N by GROUP_2:109 ;
((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (d * b)) * N by GROUP_2:105
.= [.d,b.] * N by GROUP_5:16 ;
then [.d,b.] in N by A10, GROUP_2:113;
hence x in carr N by A5, STRUCT_0:def_5; ::_thesis: verum
end;
hence commutators (G1,((Omega). G)) c= carr N by SUBSET_1:2; ::_thesis: verum
end;
gr (carr N) = N by GROUP_4:31;
hence [.G1,((Omega). G).] is Subgroup of N by A4, GROUP_4:32; ::_thesis: verum
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)
proof
let G be Group; ::_thesis: 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)
let G1 be Subgroup of G; ::_thesis: 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)
let N be normal Subgroup of G; ::_thesis: ( N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N implies G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) )
assume that
A1: N is strict Subgroup of G1 and
A2: [.G1,((Omega). G).] is strict Subgroup of N ; ::_thesis: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N)
A3: (G1,N) `*` = N by A1, GROUP_6:def_1;
reconsider J = G1 ./. ((G1,N) `*`) as Subgroup of G ./. N by A1, GROUP_6:28;
reconsider I = N as normal Subgroup of G1 by A3;
for S1 being Element of (G ./. N) st S1 in J holds
S1 in center (G ./. N)
proof
let S1 be Element of (G ./. N); ::_thesis: ( S1 in J implies S1 in center (G ./. N) )
assume A4: S1 in J ; ::_thesis: S1 in center (G ./. N)
for S being Element of (G ./. N) holds S1 * S = S * S1
proof
let S be Element of (G ./. N); ::_thesis: S1 * S = S * S1
consider a being Element of G such that
A5: ( S = a * N & S = N * a ) by GROUP_6:21;
consider c being Element of G1 such that
A6: ( S1 = c * I & S1 = I * c ) by A3, A4, GROUP_6:23;
reconsider d = c as Element of G by GROUP_2:42;
A7: d in G1 by STRUCT_0:def_5;
a in (Omega). G by STRUCT_0:def_5;
then [.d,a.] in [.G1,((Omega). G).] by A7, GROUP_5:65;
then A8: [.d,a.] in N by A2, GROUP_2:40;
A9: ( @ S = S & @ S1 = S1 & c * I = d * N & N * d = I * c ) by GROUP_6:2;
then A10: S * S1 = (a * N) * (d * N) by A5, A6, GROUP_6:def_3
.= (a * d) * N by GROUP_11:1 ;
A11: S1 * S = (d * N) * (a * N) by A5, A6, A9, GROUP_6:def_3
.= (d * a) * N by GROUP_11:1 ;
A12: ((a * d) * [.d,a.]) * N = (a * d) * ([.d,a.] * N) by GROUP_2:32
.= (a * d) * N by A8, GROUP_2:113 ;
((a * d) * [.d,a.]) * N = ((a * d) * (((d ") * (a ")) * (d * a))) * N by GROUP_1:def_3
.= (((a * d) * ((d ") * (a "))) * (d * a)) * N by GROUP_1:def_3
.= ((a * (d * ((d ") * (a ")))) * (d * a)) * N by GROUP_1:def_3
.= ((a * ((d * (d ")) * (a "))) * (d * a)) * N by GROUP_1:def_3
.= ((a * ((1_ G) * (a "))) * (d * a)) * N by GROUP_1:def_5
.= ((a * (a ")) * (d * a)) * N by GROUP_1:def_4
.= ((1_ G) * (d * a)) * N by GROUP_1:def_5
.= (d * a) * N by GROUP_1:def_4 ;
hence S1 * S = S * S1 by A10, A11, A12; ::_thesis: verum
end;
hence S1 in center (G ./. N) by GROUP_5:77; ::_thesis: verum
end;
hence G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by GROUP_2:58; ::_thesis: verum
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 ) ) ) )
proof
let G be Group; ::_thesis: ( 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 ) ) ) )
A1: now__::_thesis:_(_G_is_nilpotent_implies_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_)_)_)_)
assume G is nilpotent ; ::_thesis: 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 ) ) )
then consider R being FinSequence of the_normal_subgroups_of G such that
A2: ( len R > 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being strict normal Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) ) by Def2;
reconsider F = R as FinSequence of the_normal_subgroups_of G ;
A3: 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 strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
let G1, G2 be strict normal Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
then A6: ( G2 is strict Subgroup of G1 & ( for N being strict normal Subgroup of G st N = G2 & N is strict Subgroup of G1 holds
G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ) ) by A2, A4;
[.G1,((Omega). G).] is strict Subgroup of G2
proof
now__::_thesis:_for_N_being_strict_normal_Subgroup_of_G_st_N_=_G2_&_N_is_strict_Subgroup_of_G1_holds_
[.G1,((Omega)._G).]_is_strict_Subgroup_of_G2
let N be strict normal Subgroup of G; ::_thesis: ( N = G2 & N is strict Subgroup of G1 implies [.G1,((Omega). G).] is strict Subgroup of G2 )
assume A7: ( N = G2 & N is strict Subgroup of G1 ) ; ::_thesis: [.G1,((Omega). G).] is strict Subgroup of G2
then G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by A2, A4, A5;
hence [.G1,((Omega). G).] is strict Subgroup of G2 by A7, Th19; ::_thesis: verum
end;
hence [.G1,((Omega). G).] is strict Subgroup of G2 by A6; ::_thesis: verum
end;
hence ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) by A2, A4, A5; ::_thesis: verum
end;
take F = F; ::_thesis: ( 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 ) ) )
thus ( 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 ) ) ) by A2, A3; ::_thesis: verum
end;
now__::_thesis:_(_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_)_)_)_implies_ex_F_being_FinSequence_of_the_normal_subgroups_of_G_st_G_is_nilpotent_)
given F being FinSequence of the_normal_subgroups_of G such that A8: ( 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 ) ) ) ; ::_thesis: ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent
A9: 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 strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A10: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
let G1, G2 be strict normal Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A11: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
then A12: G2 is strict Subgroup of G1 by A8, A10;
[.G1,((Omega). G).] is strict Subgroup of G2 by A8, A10, A11;
hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by A12, Th20; ::_thesis: verum
end;
take F = F; ::_thesis: 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 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A8, A9;
hence G is nilpotent by Def2; ::_thesis: verum
end;
hence ( 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 ) ) ) ) by A1; ::_thesis: verum
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)
proof
let G be Group; ::_thesis: 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)
let H, G1 be Subgroup of G; ::_thesis: 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)
let G2 be strict normal Subgroup of G; ::_thesis: 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)
let H1 be Subgroup of H; ::_thesis: 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)
let H2 be normal Subgroup of H; ::_thesis: ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H implies H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
assume that
A1: G2 is Subgroup of G1 and
A2: G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) and
A3: ( H1 = G1 /\ H & H2 = G2 /\ H ) ; ::_thesis: H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2)
A4: [.G1,((Omega). G).] is Subgroup of G2 by A1, A2, Th19;
A5: H2 is strict Subgroup of H1 by A1, A3, GROUP_2:92;
then A6: (H1,H2) `*` = H2 by GROUP_6:def_1;
then reconsider I = H2 as normal Subgroup of H1 ;
reconsider J = H1 ./. ((H1,H2) `*`) as Subgroup of H ./. H2 by A5, GROUP_6:28;
for T being Element of (H ./. H2) st T in J holds
T in center (H ./. H2)
proof
let T be Element of (H ./. H2); ::_thesis: ( T in J implies T in center (H ./. H2) )
assume A7: T in J ; ::_thesis: T in center (H ./. H2)
for S being Element of (H ./. H2) holds S * T = T * S
proof
let S be Element of (H ./. H2); ::_thesis: S * T = T * S
consider h being Element of H such that
A8: ( S = h * H2 & S = H2 * h ) by GROUP_6:21;
consider h1 being Element of H1 such that
A9: ( T = h1 * I & T = I * h1 ) by A6, A7, GROUP_6:23;
reconsider h2 = h1 as Element of H by GROUP_2:42;
A10: ( @ S = S & @ T = T & h1 * I = h2 * H2 ) by GROUP_6:2;
then A11: S * T = (h * H2) * (h2 * H2) by A8, A9, GROUP_6:def_3
.= (h * h2) * H2 by GROUP_11:1 ;
A12: T * S = (h2 * H2) * (h * H2) by A8, A9, A10, GROUP_6:def_3
.= (h2 * h) * H2 by GROUP_11:1 ;
A13: [.h2,h.] in H by STRUCT_0:def_5;
reconsider a = h as Element of G by GROUP_2:42;
A14: a in (Omega). G by STRUCT_0:def_5;
H1 is Subgroup of G1 by A3, GROUP_2:88;
then reconsider b = h1 as Element of G1 by GROUP_2:42;
reconsider c = b as Element of G by GROUP_2:42;
b in G1 by STRUCT_0:def_5;
then [.c,a.] in [.G1,((Omega). G).] by A14, GROUP_5:65;
then A15: [.c,a.] in G2 by A4, GROUP_2:40;
A16: a " = h " by GROUP_2:48;
c " = h2 " by GROUP_2:48;
then A17: (h2 ") * (h ") = (c ") * (a ") by A16, GROUP_2:43;
h2 * h = c * a by GROUP_2:43;
then A18: ((h2 ") * (h ")) * (h2 * h) = ((c ") * (a ")) * (c * a) by A17, GROUP_2:43;
A19: [.h2,h.] = ((h2 ") * (h ")) * (h2 * h) by GROUP_5:16;
[.c,a.] = ((c ") * (a ")) * (c * a) by GROUP_5:16;
then [.h2,h.] in H2 by A3, A13, A15, A18, A19, GROUP_2:82;
then (h * h2) * H2 = (h * h2) * ([.h2,h.] * H2) by GROUP_2:113
.= (h * h2) * ((((h2 ") * (h ")) * (h2 * h)) * H2) by GROUP_5:16
.= ((h * h2) * (((h2 ") * (h ")) * (h2 * h))) * H2 by GROUP_2:32
.= (((h * h2) * ((h2 ") * (h "))) * (h2 * h)) * H2 by GROUP_1:def_3
.= ((h * (h2 * ((h2 ") * (h ")))) * (h2 * h)) * H2 by GROUP_1:def_3
.= ((h * ((h2 * (h2 ")) * (h "))) * (h2 * h)) * H2 by GROUP_1:def_3
.= ((h * ((1_ H) * (h "))) * (h2 * h)) * H2 by GROUP_1:def_5
.= ((h * (h ")) * (h2 * h)) * H2 by GROUP_1:def_4
.= ((1_ H) * (h2 * h)) * H2 by GROUP_1:def_5
.= (h2 * h) * H2 by GROUP_1:def_4 ;
hence S * T = T * S by A11, A12; ::_thesis: verum
end;
hence T in center (H ./. H2) by GROUP_5:77; ::_thesis: verum
end;
hence H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) by GROUP_2:58; ::_thesis: verum
end;
Lm4: for G being Group
for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
proof
let G be Group; ::_thesis: for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
let H be Subgroup of G; ::_thesis: ((Omega). G) /\ H = (Omega). H
reconsider G9 = (Omega). G as strict Group ;
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def_5;
then reconsider H9 = (Omega). H as strict Subgroup of G9 by GROUP_2:def_5;
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def_5;
then A1: H is Subgroup of (Omega). G by GROUP_2:def_5;
multMagma(# the carrier of (((Omega). G) /\ H), the multF of (((Omega). G) /\ H) #) = multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #)
.= multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #)
.= multMagma(# the carrier of H, the multF of H #) by A1, GROUP_2:89
.= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #) by GROUP_2:89
.= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #)
.= multMagma(# the carrier of (((Omega). G9) /\ H9), the multF of (((Omega). G9) /\ H9) #) ;
hence ((Omega). G) /\ H = (Omega). H by GROUP_2:86; ::_thesis: verum
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
let G be Group; ::_thesis: 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
let F1 be strict Subgroup of G; ::_thesis: for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
let H, F2 be Subgroup of G; ::_thesis: ( F1 is normal Subgroup of F2 implies F1 /\ H is normal Subgroup of F2 /\ H )
reconsider F = F2 /\ H as Subgroup of F2 by GROUP_2:88;
assume A1: F1 is normal Subgroup of F2 ; ::_thesis: F1 /\ H is normal Subgroup of F2 /\ H
then A2: F1 /\ H = (F1 /\ F2) /\ H by GROUP_2:89
.= F1 /\ (F2 /\ H) by GROUP_2:84 ;
reconsider F1 = F1 as normal Subgroup of F2 by A1;
F1 /\ F is normal Subgroup of F ;
hence F1 /\ H is normal Subgroup of F2 /\ H by A2, GROUP_6:3; ::_thesis: verum
end;
registration
let G be nilpotent Group;
cluster -> nilpotent for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is nilpotent
proof
let H be Subgroup of G; ::_thesis: H is nilpotent
consider F being FinSequence of the_normal_subgroups_of G such that
A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and
A2: 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2;
defpred S1[ set , set ] means ex I being strict normal Subgroup of G st
( I = F . G & c2 = I /\ H );
A3: for k being Nat st k in Seg (len F) holds
ex x being Element of the_normal_subgroups_of H st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of H st S1[k,x] )
assume k in Seg (len F) ; ::_thesis: ex x being Element of the_normal_subgroups_of H st S1[k,x]
then k in dom F by FINSEQ_1:def_3;
then F . k in the_normal_subgroups_of G by FINSEQ_2:11;
then reconsider I = F . k as strict normal Subgroup of G by Def1;
reconsider x = I /\ H as strict Subgroup of H ;
reconsider y = x as Element of the_normal_subgroups_of H by Def1;
take y ; ::_thesis: S1[k,y]
take I ; ::_thesis: ( I = F . k & y = I /\ H )
thus ( I = F . k & y = I /\ H ) ; ::_thesis: verum
end;
consider R being FinSequence of the_normal_subgroups_of H such that
A4: ( dom R = Seg (len F) & ( for i being Nat st i in Seg (len F) holds
S1[i,R . i] ) ) from FINSEQ_1:sch_5(A3);
A5: len R = len F by A4, FINSEQ_1:def_3;
A6: len R > 0 by A1, A4, FINSEQ_1:def_3;
A7: R . 1 = (Omega). H
proof
1 <= len R by A6, NAT_1:14;
then 1 in Seg (len F) by A5;
then ex I being strict normal Subgroup of G st
( I = F . 1 & R . 1 = I /\ H ) by A4;
hence R . 1 = (Omega). H by A1, Lm4; ::_thesis: verum
end;
A8: R . (len R) = (1). H
proof
ex I being strict normal Subgroup of G st
( I = F . (len R) & R . (len R) = I /\ H ) by A1, A4, A5, FINSEQ_1:3;
hence R . (len R) = (1). G by A1, A5, GROUP_2:85
.= (1). H by GROUP_2:63 ;
::_thesis: verum
end;
A9: for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) )
assume A10: ( i in dom R & i + 1 in dom R ) ; ::_thesis: for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
let H1, H2 be strict normal Subgroup of H; ::_thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) )
assume A11: ( H1 = R . i & H2 = R . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) )
consider I being strict normal Subgroup of G such that
A12: ( I = F . i & R . i = I /\ H ) by A4, A10;
consider J being strict normal Subgroup of G such that
A13: ( J = F . (i + 1) & R . (i + 1) = J /\ H ) by A4, A10;
A14: ( i in dom F & i + 1 in dom F ) by A4, A10, FINSEQ_1:def_3;
then A15: J is strict normal Subgroup of I by A12, A13, A2, GROUP_6:8;
I ./. ((I,J) `*`) is Subgroup of center (G ./. J) by A14, A12, A13, A2;
hence ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) by A13, A15, A12, A11, Th22, Lm5; ::_thesis: verum
end;
take R ; :: according to GRNILP_1:def_2 ::_thesis: ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for G1, G2 being strict normal Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) )
thus ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds
for G1, G2 being strict normal Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) by A1, A4, A7, A8, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
registration
cluster non empty Group-like associative commutative -> nilpotent for multMagma ;
correctness
coherence
for b1 being Group st b1 is commutative holds
b1 is nilpotent ;
proof
let G be Group; ::_thesis: ( G is commutative implies G is nilpotent )
assume A1: G is commutative ; ::_thesis: G is nilpotent
( (Omega). G in the_normal_subgroups_of G & (1). G in the_normal_subgroups_of G ) by Def1;
then <*((Omega). G),((1). G)*> is FinSequence of the_normal_subgroups_of G by FINSEQ_2:13;
then consider F being FinSequence of the_normal_subgroups_of G such that
A2: F = <*((Omega). G),((1). G)*> ;
A3: ( len F = 2 & F . 1 = (Omega). G & F . 2 = (1). G ) by A2, FINSEQ_1:44;
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
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies 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 ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: 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 )
now__::_thesis:_for_G1,_G2_being_Subgroup_of_G_st_G1_=_F_._i_&_G2_=_F_._(i_+_1)_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_)
let G1, G2 be Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies 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 ) )
assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: 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 )
A6: dom F = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def_3;
A7: ( i in {1,2} & i + 1 in {1,2} ) by A3, A4, FINSEQ_1:2, FINSEQ_1:def_3;
A8: ( i = 1 or i = 2 ) by A4, A6, TARSKI:def_2;
commutators (G1,((Omega). G)) = {(1_ G)} by A1, GROUP_5:57;
then A9: [.G1,((Omega). G).] = gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35
.= gr ({} the carrier of G) by XBOOLE_1:37
.= (1). G by GROUP_4:30 ;
( G1 = (Omega). G & G2 = (1). G ) by A2, A5, A7, A8, FINSEQ_1:44, TARSKI:def_2;
hence 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 ) by A5, A9, GROUP_2:65; ::_thesis: verum
end;
hence 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 ) ; ::_thesis: verum
end;
hence G is nilpotent by A3, Th21; ::_thesis: verum
end;
cluster non empty Group-like associative cyclic -> nilpotent for multMagma ;
coherence
for b1 being Group st b1 is cyclic holds
b1 is nilpotent ;
end;
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) )
proof
let G, H be strict Group; ::_thesis: 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) )
let h be Homomorphism of G,H; ::_thesis: 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) )
let A be strict Subgroup of G; ::_thesis: 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) )
let a, b be Element of G; ::_thesis: ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )
thus ((h . a) * (h . b)) * (h .: A) = (h . (a * b)) * (h .: A) by GROUP_6:def_6
.= h .: ((a * b) * A) by GRSOLV_1:13 ; ::_thesis: ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b)
thus ((h .: A) * (h . a)) * (h . b) = (h .: A) * ((h . a) * (h . b)) by GROUP_2:107
.= (h .: A) * (h . (a * b)) by GROUP_6:def_6
.= h .: (A * (a * b)) by GRSOLV_1:13
.= h .: ((A * a) * b) by GROUP_2:107 ; ::_thesis: verum
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)
proof
let G, H be strict Group; ::_thesis: 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)
let h be Homomorphism of G,H; ::_thesis: 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)
let A be strict Subgroup of G; ::_thesis: 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)
let a, b be Element of G; ::_thesis: 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)
let H1 be Subgroup of Image h; ::_thesis: 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)
let a1, b1 be Element of (Image h); ::_thesis: ( a1 = h . a & b1 = h . b & H1 = h .: A implies (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) )
assume that
A1: a1 = h . a and
A2: b1 = h . b and
A3: H1 = h .: A ; ::_thesis: (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)
A4: a1 * b1 = (h . a) * (h . b) by A1, A2, GROUP_2:43;
set c1 = a1 * b1;
set c = a * b;
A5: h . (a * b) = (h . a) * (h . b) by GROUP_6:def_6;
A6: h .: ((a * b) * A) = (h . (a * b)) * (h .: A) by GRSOLV_1:13;
(a1 * b1) * H1 = (h . (a * b)) * (h .: A)
proof
now__::_thesis:_for_x_being_set_st_x_in_(a1_*_b1)_*_H1_holds_
x_in_(h_._(a_*_b))_*_(h_.:_A)
let x be set ; ::_thesis: ( x in (a1 * b1) * H1 implies x in (h . (a * b)) * (h .: A) )
assume x in (a1 * b1) * H1 ; ::_thesis: x in (h . (a * b)) * (h .: A)
then consider Z being Element of (Image h) such that
A7: x = (a1 * b1) * Z and
A8: Z in H1 by GROUP_2:103;
consider Z1 being Element of A such that
A9: Z = (h | A) . Z1 by A3, A8, GROUP_6:45;
A10: Z1 in A by STRUCT_0:def_5;
reconsider Z1 = Z1 as Element of G by GROUP_2:42;
Z = h . Z1 by A9, FUNCT_1:49;
then A11: x = (h . (a * b)) * (h . Z1) by A4, A5, A7, GROUP_2:43
.= h . ((a * b) * Z1) by GROUP_6:def_6 ;
(a * b) * Z1 in (a * b) * A by A10, GROUP_2:103;
hence x in (h . (a * b)) * (h .: A) by A11, A6, FUNCT_2:35; ::_thesis: verum
end;
then A12: (a1 * b1) * H1 c= (h . (a * b)) * (h .: A) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(h_._(a_*_b))_*_(h_.:_A)_holds_
x_in_(a1_*_b1)_*_H1
let x be set ; ::_thesis: ( x in (h . (a * b)) * (h .: A) implies x in (a1 * b1) * H1 )
assume x in (h . (a * b)) * (h .: A) ; ::_thesis: x in (a1 * b1) * H1
then consider y being set such that
A13: y in the carrier of G and
A14: y in (a * b) * A and
A15: x = h . y by A6, FUNCT_2:64;
reconsider y = y as Element of G by A13;
consider Z being Element of G such that
A16: y = (a * b) * Z and
A17: Z in A by A14, GROUP_2:103;
Z in the carrier of A by A17, STRUCT_0:def_5;
then h . Z in h .: the carrier of A by FUNCT_2:35;
then h . Z in the carrier of (h .: A) by GRSOLV_1:8;
then A18: h . Z in H1 by A3, STRUCT_0:def_5;
then h . Z in Image h by GROUP_2:40;
then reconsider Z1 = h . Z as Element of (Image h) by STRUCT_0:def_5;
x = (h . (a * b)) * (h . Z) by A15, A16, GROUP_6:def_6;
then x = (a1 * b1) * Z1 by A4, A5, GROUP_2:43;
hence x in (a1 * b1) * H1 by A18, GROUP_2:103; ::_thesis: verum
end;
then (h . (a * b)) * (h .: A) c= (a1 * b1) * H1 by TARSKI:def_3;
hence (a1 * b1) * H1 = (h . (a * b)) * (h .: A) by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
hence (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) by GROUP_6:def_6; ::_thesis: verum
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)
proof
let G, H be strict Group; ::_thesis: 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)
let h be Homomorphism of G,H; ::_thesis: 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)
let G1 be strict Subgroup of G; ::_thesis: 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)
let G2 be strict normal Subgroup of G; ::_thesis: 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)
let H1 be strict Subgroup of Image h; ::_thesis: 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)
let H2 be strict normal Subgroup of Image h; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 implies H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
assume that
A1: G2 is strict Subgroup of G1 and
A2: G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) and
A3: ( H1 = h .: G1 & H2 = h .: G2 ) ; ::_thesis: H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2)
A4: H2 is strict Subgroup of H1 by A1, A3, GRSOLV_1:12;
then A5: (H1,H2) `*` = H2 by GROUP_6:def_1;
then reconsider I = H2 as normal Subgroup of H1 ;
reconsider J = H1 ./. ((H1,H2) `*`) as Subgroup of (Image h) ./. H2 by A4, GROUP_6:28;
for T being Element of ((Image h) ./. H2) st T in J holds
T in center ((Image h) ./. H2)
proof
let T be Element of ((Image h) ./. H2); ::_thesis: ( T in J implies T in center ((Image h) ./. H2) )
assume A6: T in J ; ::_thesis: T in center ((Image h) ./. H2)
for S being Element of ((Image h) ./. H2) holds S * T = T * S
proof
let S be Element of ((Image h) ./. H2); ::_thesis: S * T = T * S
consider g being Element of (Image h) such that
A7: ( S = g * H2 & S = H2 * g ) by GROUP_6:21;
consider h1 being Element of H1 such that
A8: ( T = h1 * I & T = I * h1 ) by A5, A6, GROUP_6:23;
reconsider h2 = h1 as Element of (Image h) by GROUP_2:42;
A9: ( @ S = S & @ T = T & h1 * I = h2 * H2 ) by GROUP_6:2;
then A10: S * T = (g * H2) * (h2 * H2) by A7, A8, GROUP_6:def_3
.= (g * h2) * H2 by GROUP_11:1 ;
A11: T * S = (h2 * H2) * (g * H2) by A7, A8, A9, GROUP_6:def_3
.= (h2 * g) * H2 by GROUP_11:1 ;
g in Image h by STRUCT_0:def_5;
then consider a being Element of G such that
A12: g = h . a by GROUP_6:45;
A13: a in (Omega). G by STRUCT_0:def_5;
h1 in H1 by STRUCT_0:def_5;
then consider a1 being Element of G1 such that
A14: h1 = (h | G1) . a1 by A3, GROUP_6:45;
A15: a1 in G1 by STRUCT_0:def_5;
reconsider a2 = a1 as Element of G by GROUP_2:42;
A16: h2 = h . a2 by A14, FUNCT_1:49;
then A17: (g * h2) * H2 = ((h . a) * (h . a2)) * (h .: G2) by A12, A3, Th24
.= h .: ((a * a2) * G2) by Th23 ;
A18: (h2 * g) * H2 = ((h . a2) * (h . a)) * (h .: G2) by A12, A16, A3, Th24
.= h .: ((a2 * a) * G2) by Th23 ;
A19: [.G1,((Omega). G).] is strict Subgroup of G2 by A1, A2, Th19;
[.a2,a.] in [.G1,((Omega). G).] by A13, A15, GROUP_5:65;
then [.a2,a.] in G2 by A19, GROUP_2:40;
then (a * a2) * G2 = (a * a2) * ([.a2,a.] * G2) by GROUP_2:113
.= (a * a2) * ((((a2 ") * (a ")) * (a2 * a)) * G2) by GROUP_5:16
.= ((a * a2) * (((a2 ") * (a ")) * (a2 * a))) * G2 by GROUP_2:32
.= (((a * a2) * ((a2 ") * (a "))) * (a2 * a)) * G2 by GROUP_1:def_3
.= ((a * (a2 * ((a2 ") * (a ")))) * (a2 * a)) * G2 by GROUP_1:def_3
.= ((a * ((a2 * (a2 ")) * (a "))) * (a2 * a)) * G2 by GROUP_1:def_3
.= ((a * ((1_ G) * (a "))) * (a2 * a)) * G2 by GROUP_1:def_5
.= ((a * (a ")) * (a2 * a)) * G2 by GROUP_1:def_4
.= ((1_ G) * (a2 * a)) * G2 by GROUP_1:def_5
.= (a2 * a) * G2 by GROUP_1:def_4 ;
hence S * T = T * S by A10, A11, A17, A18; ::_thesis: verum
end;
hence T in center ((Image h) ./. H2) by GROUP_5:77; ::_thesis: verum
end;
hence H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) by GROUP_2:58; ::_thesis: verum
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
proof
let G, H be strict Group; ::_thesis: 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
let h be Homomorphism of G,H; ::_thesis: for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h
let A be strict normal Subgroup of G; ::_thesis: h .: A is strict normal Subgroup of Image h
reconsider C = h .: A as strict Subgroup of Image h by GRSOLV_1:9;
for b being Element of (Image h) holds b * C c= C * b
proof
let b be Element of (Image h); ::_thesis: b * C c= C * b
A1: b in Image h by STRUCT_0:def_5;
now__::_thesis:_for_x_being_set_st_x_in_b_*_C_holds_
x_in_C_*_b
consider b1 being Element of G such that
A2: b = h . b1 by A1, GROUP_6:45;
let x be set ; ::_thesis: ( x in b * C implies x in C * b )
assume x in b * C ; ::_thesis: x in C * b
then consider g being Element of (Image h) such that
A3: x = b * g and
A4: g in C by GROUP_2:103;
consider g1 being Element of A such that
A5: g = (h | A) . g1 by A4, GROUP_6:45;
reconsider g1 = g1 as Element of G by GROUP_2:42;
g = h . g1 by A5, FUNCT_1:49;
then A6: x = (h . b1) * (h . g1) by A2, A3, GROUP_2:43
.= h . (b1 * g1) by GROUP_6:def_6 ;
g1 in A by STRUCT_0:def_5;
then A7: b1 * g1 in b1 * A by GROUP_2:103;
A8: h .: (A * b1) = (h .: A) * (h . b1) by GRSOLV_1:13;
b1 * A = A * b1 by GROUP_3:117;
then x in (h .: A) * (h . b1) by A6, A7, A8, FUNCT_2:35;
hence x in C * b by A2, GROUP_6:2; ::_thesis: verum
end;
hence b * C c= C * b by TARSKI:def_3; ::_thesis: verum
end;
hence h .: A is strict normal Subgroup of Image h by GROUP_3:118; ::_thesis: verum
end;
registration
let G be strict nilpotent Group;
let H be strict Group;
let h be Homomorphism of G,H;
cluster Image h -> nilpotent ;
coherence
Image h is nilpotent
proof
consider F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 and
A2: F . 1 = (Omega). G and
A3: F . (len F) = (1). G and
A4: 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2;
1 <= len F by A1, NAT_1:14;
then A5: 1 in Seg (len F) ;
defpred S1[ set , set ] means ex J being strict normal Subgroup of G st
( J = F . G & H = h .: J );
A6: for k being Nat st k in Seg (len F) holds
ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] )
assume k in Seg (len F) ; ::_thesis: ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x]
then k in dom F by FINSEQ_1:def_3;
then F . k in the_normal_subgroups_of G by FINSEQ_2:11;
then F . k is strict normal Subgroup of G by Def1;
then consider A being strict normal Subgroup of G such that
A7: A = F . k ;
h .: A is strict normal Subgroup of Image h by Th26;
then h .: A in the_normal_subgroups_of (Image h) by Def1;
hence ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] by A7; ::_thesis: verum
end;
consider Z being FinSequence of the_normal_subgroups_of (Image h) such that
A8: ( dom Z = Seg (len F) & ( for j being Nat st j in Seg (len F) holds
S1[j,Z . j] ) ) from FINSEQ_1:sch_5(A6);
Seg (len Z) = Seg (len F) by A8, FINSEQ_1:def_3;
then A9: dom F = Seg (len Z) by FINSEQ_1:def_3
.= dom Z by FINSEQ_1:def_3 ;
A10: for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom Z & i + 1 in dom Z implies for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) )
assume A11: ( i in dom Z & i + 1 in dom Z ) ; ::_thesis: for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
let H1, H2 be strict normal Subgroup of Image h; ::_thesis: ( H1 = Z . i & H2 = Z . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) )
assume that
A12: H1 = Z . i and
A13: H2 = Z . (i + 1) ; ::_thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) )
A14: ( i in dom F & i + 1 in dom F ) by A8, A11, FINSEQ_1:def_3;
consider G1 being strict normal Subgroup of G such that
A15: G1 = F . i and
A16: H1 = h .: G1 by A8, A11, A12;
consider G2 being strict normal Subgroup of G such that
A17: G2 = F . (i + 1) and
A18: H2 = h .: G2 by A8, A11, A13;
A19: G2 is strict Subgroup of G1 by A4, A9, A11, A15, A17;
G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) by A14, A15, A17, A4;
hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) by A16, A19, A18, Th25, GRSOLV_1:12; ::_thesis: verum
end;
take Z ; :: according to GRNILP_1:def_2 ::_thesis: ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) )
A20: len Z = len F by A8, FINSEQ_1:def_3;
( Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) )
proof
ex G1 being strict normal Subgroup of G st
( G1 = F . 1 & Z . 1 = h .: G1 ) by A8, A5;
hence Z . 1 = (Omega). (Image h) by A2, GRSOLV_1:11; ::_thesis: Z . (len Z) = (1). (Image h)
ex G2 being strict normal Subgroup of G st
( G2 = F . (len F) & Z . (len F) = h .: G2 ) by A1, A8, FINSEQ_1:3;
hence Z . (len Z) = (1). H by A3, A20, GRSOLV_1:11
.= (1). (Image h) by GROUP_2:63 ;
::_thesis: verum
end;
hence ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds
for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) ) by A1, A8, A10, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
registration
let G be strict nilpotent Group;
let N be strict normal Subgroup of G;
clusterG ./. N -> nilpotent ;
coherence
G ./. N is nilpotent
proof
Image (nat_hom N) = G ./. N by GROUP_6:48;
hence G ./. N is nilpotent ; ::_thesis: verum
end;
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
proof
let G be Group; ::_thesis: ( 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) ) ) implies G is nilpotent )
given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and
A2: 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) ; ::_thesis: G is nilpotent
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) )
assume A3: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 )
let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) )
assume ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 )
then H2 = [.H1,((Omega). G).] by A2, A3;
hence ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) by Th15, GROUP_2:54; ::_thesis: verum
end;
hence G is nilpotent by A1, Th21; ::_thesis: verum
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
proof
let G be Group; ::_thesis: ( 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 ) ) ) implies G is nilpotent )
given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and
A2: 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 ) ; ::_thesis: G is nilpotent
A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A5: ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
then H2 is Subgroup of H1 by A2, A4;
then A6: H1 ./. ((H1,H2) `*`) is Subgroup of G ./. H2 by GROUP_6:28;
G ./. H2 is commutative Group by A2, A4, A5;
hence ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) by A2, A4, A5, A6, GROUP_5:82; ::_thesis: verum
end;
take F ; :: according to GRNILP_1:def_2 ::_thesis: ( 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) )
thus ( 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A1, A3; ::_thesis: verum
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
proof
let G be Group; ::_thesis: ( 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 ) ) ) implies G is nilpotent )
given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and
A2: 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 ) ; ::_thesis: G is nilpotent
A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A5: ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
then H2 is strict Subgroup of H1 by A2, A4;
then A6: H1 ./. ((H1,H2) `*`) is Subgroup of G ./. H2 by GROUP_6:28;
G ./. H2 is commutative Group by A2, A4, A5;
hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) by A2, A4, A5, A6, GROUP_5:82; ::_thesis: verum
end;
take F ; :: according to GRNILP_1:def_2 ::_thesis: ( 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) )
thus ( 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A1, A3; ::_thesis: verum
end;
registration
cluster non empty Group-like associative nilpotent -> solvable for multMagma ;
correctness
coherence
for b1 being Group st b1 is nilpotent holds
b1 is solvable ;
proof
let G be Group; ::_thesis: ( G is nilpotent implies G is solvable )
assume G is nilpotent ; ::_thesis: G is solvable
then consider F being FinSequence of the_normal_subgroups_of G such that
A1: ( 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 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by Def2;
reconsider R = F as FinSequence of Subgroups G by Th18;
A2: for i being Element of NAT st i in dom R & i + 1 in dom R holds
for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A3: ( i in dom R & i + 1 in dom R ) ; ::_thesis: for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds
( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
then A4: ( F . i is strict normal Subgroup of G & F . (i + 1) is strict normal Subgroup of G ) by Th16;
let H1, H2 be Subgroup of G; ::_thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) )
assume A5: ( H1 = R . i & H2 = R . (i + 1) ) ; ::_thesis: ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) )
for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative
proof
let N be normal Subgroup of H1; ::_thesis: ( N = H2 implies H1 ./. N is commutative )
assume A6: N = H2 ; ::_thesis: H1 ./. N is commutative
then reconsider N9 = N as strict normal Subgroup of G by A5, A4;
A7: H1 ./. ((H1,N9) `*`) is Subgroup of center (G ./. N9) by A1, A3, A5, A6, A4;
center (G ./. N9) is commutative by GROUP_5:80;
hence H1 ./. N is commutative by A7, GROUP_6:def_1; ::_thesis: verum
end;
hence ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) by A1, A3, A5, A4, GROUP_6:8; ::_thesis: verum
end;
take R ; :: according to GRSOLV_1:def_1 ::_thesis: ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds
( not b1 in dom R or not K403(b1,1) in dom R or for b2, b3 being Subgroup of G holds
( not b2 = R . b1 or not b3 = R . K403(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds
( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) )
thus ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds
( not b1 in dom R or not K403(b1,1) in dom R or for b2, b3 being Subgroup of G holds
( not b2 = R . b1 or not b3 = R . K403(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds
( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) ) by A1, A2; ::_thesis: verum
end;
end;