let G be Group; for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
let N1, N2 be normal Subgroup of G; [.N1,N2.] is Subgroup of [.N2,N1.]
now for a being Element of G st a in [.N1,N2.] holds
a in [.N2,N1.]let a be
Element of
G;
( a in [.N1,N2.] implies a in [.N2,N1.] )assume
a in [.N1,N2.]
;
a in [.N2,N1.]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 (
N1,
N2)
and A2:
a = Product (F |^ I)
by Th61;
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 F = Seg (len F)
by FINSEQ_1:def 3;
A6:
rng F1 c= commutators (
N2,
N1)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng F1 or x in commutators (N2,N1) )
assume
x in rng F1
;
x in commutators (N2,N1)
then consider y being
object such that A7:
y in dom F1
and A8:
F1 . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A7;
y in dom F
by A3, A7, FINSEQ_3:29;
then A9:
F /. y = F . y
by PARTFUN1:def 6;
y in dom F
by A3, A7, FINSEQ_3:29;
then
F . y in rng F
by FUNCT_1:def 3;
then consider b,
c being
Element of
G such that A10:
F . y = [.b,c.]
and A11:
(
b in N1 &
c in N2 )
by A1, Th52;
x = (F /. y) "
by A4, A7, A8;
then
x = [.c,b.]
by A10, A9, Th22;
hence
x in commutators (
N2,
N1)
by A11, Th52;
verum
end; A12:
len (F |^ I) = len F
by GROUP_4:def 3;
then A13:
dom (F |^ I) = Seg (len F)
by FINSEQ_1:def 3;
deffunc H2(
Nat)
-> Element of
INT =
@ (- (@ (I /. $1)));
consider I1 being
FinSequence of
INT such that A14:
len I1 = len F
and A15:
for
k being
Nat st
k in dom I1 holds
I1 . k = H2(
k)
from FINSEQ_2:sch 1();
set J =
F1 |^ I1;
A16:
dom F1 = dom F
by A3, FINSEQ_3:29;
A17:
dom I1 = dom F
by A14, FINSEQ_3:29;
A18:
now for k being Nat st k in dom (F |^ I) holds
(F |^ I) . k = (F1 |^ I1) . klet k be
Nat;
( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )assume A19:
k in dom (F |^ I)
;
(F |^ I) . k = (F1 |^ I1) . kthen A20:
k in dom F
by A13, FINSEQ_1:def 3;
A21:
(
(F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) &
F1 /. k = F1 . k )
by A5, A16, A13, A19, GROUP_4:def 3, PARTFUN1:def 6;
A22:
I1 . k = @ (- (@ (I /. k)))
by A15, A5, A17, A13, A19;
(
F1 . k = (F /. k) " &
I1 . k = I1 /. k )
by A4, A5, A16, A17, A13, A19, PARTFUN1:def 6;
then (F1 |^ I1) . k =
(((F /. k) ") |^ (@ (I /. k))) "
by A21, A22, GROUP_1:36
.=
(((F /. k) |^ (@ (I /. k))) ") "
by GROUP_1:37
.=
(F /. k) |^ (@ (I /. k))
;
hence
(F |^ I) . k = (F1 |^ I1) . k
by A20, GROUP_4:def 3;
verum end;
len (F1 |^ I1) = len F
by A3, GROUP_4:def 3;
then
F1 |^ I1 = F |^ I
by A12, A18, FINSEQ_2:9;
hence
a in [.N2,N1.]
by A2, A3, A14, A6, Th61;
verum end;
hence
[.N1,N2.] is Subgroup of [.N2,N1.]
by GROUP_2:58; verum