let G be 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)
let H, G1 be 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 G2 be 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 H1 be 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 H2 be normal Subgroup of H; ( 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 )
; H1 ./. (H1,H2 `*` ) is Subgroup of center (H ./. H2)
A4:
[.G1,((Omega). G).] is Subgroup of G2
by A1, A2, Th22;
B:
H2 is strict Subgroup of H1
by A1, A3, GROUP_2:110;
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 H ./. H2 by B, GROUP_6:34;
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);
( T in J implies T in center (H ./. H2) )
assume A6:
T in J
;
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);
S * T = T * S
consider h being
Element of
H such that A7:
(
S = h * H2 &
S = H2 * h )
by GROUP_6:26;
consider h1 being
Element of
H1 such that A8:
(
T = h1 * I &
T = I * h1 )
by A5, A6, GROUP_6:28;
reconsider h2 =
h1 as
Element of
H by GROUP_2:51;
A9:
(
@ S = S &
@ T = T &
h1 * I = h2 * H2 )
by GROUP_6:2;
then A10:
S * T =
(h * H2) * (h2 * H2)
by A7, A8, GROUP_6:def 4
.=
(h * h2) * H2
by GROUP_11:1
;
A11:
T * S =
(h2 * H2) * (h * H2)
by A7, A8, A9, GROUP_6:def 4
.=
(h2 * h) * H2
by GROUP_11:1
;
A12:
[.h2,h.] in H
by STRUCT_0:def 5;
reconsider a =
h as
Element of
G by GROUP_2:51;
A13:
a in (Omega). G
by STRUCT_0:def 5;
H1 is
Subgroup of
G1
by A3, GROUP_2:106;
then reconsider b =
h1 as
Element of
G1 by GROUP_2:51;
reconsider c =
b as
Element of
G by GROUP_2:51;
b in G1
by STRUCT_0:def 5;
then
[.c,a.] in [.G1,((Omega). G).]
by A13, GROUP_5:74;
then A14:
[.c,a.] in G2
by A4, GROUP_2:49;
A15:
a " = h "
by GROUP_2:57;
c " = h2 "
by GROUP_2:57;
then A17:
(h2 " ) * (h " ) = (c " ) * (a " )
by A15, GROUP_2:52;
h2 * h = c * a
by GROUP_2:52;
then A18:
((h2 " ) * (h " )) * (h2 * h) = ((c " ) * (a " )) * (c * a)
by A17, GROUP_2:52;
A19:
[.h2,h.] = ((h2 " ) * (h " )) * (h2 * h)
by GROUP_5:19;
[.c,a.] = ((c " ) * (a " )) * (c * a)
by GROUP_5:19;
then
[.h2,h.] in H2
by A3, A12, A14, A18, A19, GROUP_2:99;
then (h * h2) * H2 =
(h * h2) * ([.h2,h.] * H2)
by GROUP_2:136
.=
(h * h2) * ((((h2 " ) * (h " )) * (h2 * h)) * H2)
by GROUP_5:19
.=
((h * h2) * (((h2 " ) * (h " )) * (h2 * h))) * H2
by GROUP_2:38
.=
(((h * h2) * ((h2 " ) * (h " ))) * (h2 * h)) * H2
by GROUP_1:def 4
.=
((h * (h2 * ((h2 " ) * (h " )))) * (h2 * h)) * H2
by GROUP_1:def 4
.=
((h * ((h2 * (h2 " )) * (h " ))) * (h2 * h)) * H2
by GROUP_1:def 4
.=
((h * ((1_ H) * (h " ))) * (h2 * h)) * H2
by GROUP_1:def 6
.=
((h * (h " )) * (h2 * h)) * H2
by GROUP_1:def 5
.=
((1_ H) * (h2 * h)) * H2
by GROUP_1:def 6
.=
(h2 * h) * H2
by GROUP_1:def 5
;
hence
S * T = T * S
by A10, A11;
verum
end;
hence
T in center (H ./. H2)
by GROUP_5:89;
verum
end;
hence
H1 ./. (H1,H2 `*` ) is Subgroup of center (H ./. H2)
by GROUP_2:67; verum