let G, H be strict Group; for h being Homomorphism of G,H
for G1 being strict Subgroup of G
for G2 being strict normal Subgroup of G
for H1 being strict Subgroup of Image h
for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
let h be Homomorphism of G,H; for G1 being strict Subgroup of G
for G2 being strict normal Subgroup of G
for H1 being strict Subgroup of Image h
for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
let G1 be strict Subgroup of G; for G2 being strict normal Subgroup of G
for H1 being strict Subgroup of Image h
for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
let G2 be strict normal Subgroup of G; for H1 being strict Subgroup of Image h
for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
let H1 be strict Subgroup of Image h; for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
let H2 be strict normal Subgroup of Image h; ( G2 is strict Subgroup of G1 & G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 implies H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2) )
assume that
A1:
G2 is strict Subgroup of G1
and
A2:
G1 ./. (G1,G2 `*` ) is Subgroup of center (G ./. G2)
and
A3:
( H1 = h .: G1 & H2 = h .: G2 )
; H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
B:
H2 is strict Subgroup of H1
by A1, A3, GRSOLV_1:13;
then A4:
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 (Image h) ./. H2 by B, GROUP_6:34;
for T being Element of ((Image h) ./. H2) st T in J holds
T in center ((Image h) ./. H2)
proof
let T be
Element of
((Image h) ./. H2);
( T in J implies T in center ((Image h) ./. H2) )
assume A5:
T in J
;
T in center ((Image h) ./. H2)
for
S being
Element of
((Image h) ./. H2) holds
S * T = T * S
proof
let S be
Element of
((Image h) ./. H2);
S * T = T * S
consider g being
Element of
(Image h) such that A6:
(
S = g * H2 &
S = H2 * g )
by GROUP_6:26;
consider h1 being
Element of
H1 such that A7:
(
T = h1 * I &
T = I * h1 )
by A4, A5, GROUP_6:28;
reconsider h2 =
h1 as
Element of
(Image h) by GROUP_2:51;
A8:
(
@ S = S &
@ T = T &
h1 * I = h2 * H2 )
by GROUP_6:2;
then A9:
S * T =
(g * H2) * (h2 * H2)
by A6, A7, GROUP_6:def 4
.=
(g * h2) * H2
by GROUP_11:1
;
A10:
T * S =
(h2 * H2) * (g * H2)
by A6, A7, A8, GROUP_6:def 4
.=
(h2 * g) * H2
by GROUP_11:1
;
g in Image h
by STRUCT_0:def 5;
then consider a being
Element of
G such that A11:
g = h . a
by GROUP_6:54;
A12:
a in (Omega). G
by STRUCT_0:def 5;
h1 in H1
by STRUCT_0:def 5;
then consider a1 being
Element of
G1 such that A13:
h1 = (h | G1) . a1
by A3, GROUP_6:54;
A14:
a1 in G1
by STRUCT_0:def 5;
reconsider a2 =
a1 as
Element of
G by GROUP_2:51;
A15:
h2 = h . a2
by A13, FUNCT_1:72;
then A16:
(g * h2) * H2 =
((h . a) * (h . a2)) * (h .: G2)
by A11, A3, Th31
.=
h .: ((a * a2) * G2)
by Th30
;
A17:
(h2 * g) * H2 =
((h . a2) * (h . a)) * (h .: G2)
by A11, A15, A3, Th31
.=
h .: ((a2 * a) * G2)
by Th30
;
A18:
[.G1,((Omega). G).] is
strict Subgroup of
G2
by A1, A2, Th22;
[.a2,a.] in [.G1,((Omega). G).]
by A12, A14, GROUP_5:74;
then
[.a2,a.] in G2
by A18, GROUP_2:49;
then (a * a2) * G2 =
(a * a2) * ([.a2,a.] * G2)
by GROUP_2:136
.=
(a * a2) * ((((a2 " ) * (a " )) * (a2 * a)) * G2)
by GROUP_5:19
.=
((a * a2) * (((a2 " ) * (a " )) * (a2 * a))) * G2
by GROUP_2:38
.=
(((a * a2) * ((a2 " ) * (a " ))) * (a2 * a)) * G2
by GROUP_1:def 4
.=
((a * (a2 * ((a2 " ) * (a " )))) * (a2 * a)) * G2
by GROUP_1:def 4
.=
((a * ((a2 * (a2 " )) * (a " ))) * (a2 * a)) * G2
by GROUP_1:def 4
.=
((a * ((1_ G) * (a " ))) * (a2 * a)) * G2
by GROUP_1:def 6
.=
((a * (a " )) * (a2 * a)) * G2
by GROUP_1:def 5
.=
((1_ G) * (a2 * a)) * G2
by GROUP_1:def 6
.=
(a2 * a) * G2
by GROUP_1:def 5
;
hence
S * T = T * S
by A9, A10, A16, A17;
verum
end;
hence
T in center ((Image h) ./. H2)
by GROUP_5:89;
verum
end;
hence
H1 ./. (H1,H2 `*` ) is Subgroup of center ((Image h) ./. H2)
by GROUP_2:67; verum