let G be 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)
let G1 be 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 N be normal Subgroup of G; ( 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
; 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:34;
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);
( S1 in J implies S1 in center (G ./. N) )
assume A4:
S1 in J
;
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);
S1 * S = S * S1
consider a being
Element of
G such that A5:
(
S = a * N &
S = N * a )
by GROUP_6:26;
consider c being
Element of
G1 such that A6:
(
S1 = c * I &
S1 = I * c )
by A3, A4, GROUP_6:28;
reconsider d =
c as
Element of
G by GROUP_2:51;
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:74;
then A8:
[.d,a.] in N
by A2, GROUP_2:49;
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 4
.=
(a * d) * N
by GROUP_11:1
;
A11:
S1 * S =
(d * N) * (a * N)
by A5, A6, A9, GROUP_6:def 4
.=
(d * a) * N
by GROUP_11:1
;
A12:
((a * d) * [.d,a.]) * N =
(a * d) * ([.d,a.] * N)
by GROUP_2:38
.=
(a * d) * N
by A8, GROUP_2:136
;
((a * d) * [.d,a.]) * N =
((a * d) * (((d " ) * (a " )) * (d * a))) * N
by GROUP_1:def 4
.=
(((a * d) * ((d " ) * (a " ))) * (d * a)) * N
by GROUP_1:def 4
.=
((a * (d * ((d " ) * (a " )))) * (d * a)) * N
by GROUP_1:def 4
.=
((a * ((d * (d " )) * (a " ))) * (d * a)) * N
by GROUP_1:def 4
.=
((a * ((1_ G) * (a " ))) * (d * a)) * N
by GROUP_1:def 6
.=
((a * (a " )) * (d * a)) * N
by GROUP_1:def 5
.=
((1_ G) * (d * a)) * N
by GROUP_1:def 6
.=
(d * a) * N
by GROUP_1:def 5
;
hence
S1 * S = S * S1
by A10, A11, A12;
verum
end;
hence
S1 in center (G ./. N)
by GROUP_5:89;
verum
end;
hence
G1 ./. (G1,N `*` ) is Subgroup of center (G ./. N)
by GROUP_2:67; verum