let G be Group; for N1, N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G
let N1, N2 be strict normal Subgroup of G; [.N1,N2.] is normal Subgroup of G
now for a being Element of G holds [.N1,N2.] |^ a is Subgroup of [.N1,N2.]let a be
Element of
G;
[.N1,N2.] |^ a is Subgroup of [.N1,N2.]now for b being Element of G st b in [.N1,N2.] |^ a holds
b in [.N1,N2.]let b be
Element of
G;
( b in [.N1,N2.] |^ a implies b in [.N1,N2.] )assume
b in [.N1,N2.] |^ a
;
b in [.N1,N2.]then consider c being
Element of
G such that A1:
b = c |^ a
and A2:
c in [.N1,N2.]
by GROUP_3:58;
consider F being
FinSequence of the
carrier of
G,
I being
FinSequence of
INT such that A3:
len F = len I
and A4:
rng F c= commutators (
(carr N1),
(carr N2))
and A5:
c = Product (F |^ I)
by A2, GROUP_4:28;
A6:
len (F |^ a) = len F
by Def1;
A7:
rng (F |^ a) c= commutators (
(carr N1),
(carr N2))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (F |^ a) or x in commutators ((carr N1),(carr N2)) )
assume
x in rng (F |^ a)
;
x in commutators ((carr N1),(carr N2))
then consider y being
object such that A8:
y in dom (F |^ a)
and A9:
(F |^ a) . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A8;
A10:
y in dom F
by A6, A8, FINSEQ_3:29;
then A11:
F . y = F /. y
by PARTFUN1:def 6;
y in dom F
by A6, A8, FINSEQ_3:29;
then
F . y in rng F
by FUNCT_1:def 3;
then consider d,
e being
Element of
G such that A12:
F . y = [.d,e.]
and A13:
d in carr N1
and A14:
e in carr N2
by A4, Th47;
d in N1
by A13, STRUCT_0:def 5;
then
d |^ a in N1 |^ a
by GROUP_3:58;
then
d |^ a in N1
by GROUP_3:def 13;
then A15:
d |^ a in carr N1
by STRUCT_0:def 5;
e in N2
by A14, STRUCT_0:def 5;
then
e |^ a in N2 |^ a
by GROUP_3:58;
then
e |^ a in N2
by GROUP_3:def 13;
then A16:
e |^ a in carr N2
by STRUCT_0:def 5;
x = (F /. y) |^ a
by A9, A10, Def1;
then
x = [.(d |^ a),(e |^ a).]
by A12, A11, Th23;
hence
x in commutators (
(carr N1),
(carr N2))
by A15, A16;
verum
end; b =
Product ((F |^ I) |^ a)
by A1, A5, Th14
.=
Product ((F |^ a) |^ I)
by Th15
;
hence
b in [.N1,N2.]
by A3, A6, A7, GROUP_4:28;
verum end; hence
[.N1,N2.] |^ a is
Subgroup of
[.N1,N2.]
by GROUP_2:58;
verum end;
hence
[.N1,N2.] is normal Subgroup of G
by GROUP_3:122; verum