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, 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);
( T in J implies T in center (H ./. H2) )
assume A7:
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 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;
verum
end;
hence
T in center (H ./. H2)
by GROUP_5:77;
verum
end;
hence
H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2)
by GROUP_2:58; verum