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)
A4:
H2 is strict Subgroup of H1
by A1, A3, GRSOLV_1:12;
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 (Image h) ./. H2 by A4, GROUP_6:28;
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 A6:
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 A7:
(
S = g * H2 &
S = H2 * g )
by GROUP_6:21;
consider h1 being
Element of
H1 such that A8:
(
T = h1 * I &
T = I * h1 )
by A5, A6, GROUP_6:23;
reconsider h2 =
h1 as
Element of
(Image h) by GROUP_2:42;
A9:
(
@ S = S &
@ T = T &
h1 * I = h2 * H2 )
by GROUP_6:2;
then A10:
S * T =
(g * H2) * (h2 * H2)
by A7, A8, GROUP_6:def 3
.=
(g * h2) * H2
by GROUP_11:1
;
A11:
T * S =
(h2 * H2) * (g * H2)
by A7, A8, A9, GROUP_6:def 3
.=
(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 A12:
g = h . a
by GROUP_6:45;
A13:
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 A14:
h1 = (h | G1) . a1
by A3, GROUP_6:45;
A15:
a1 in G1
by STRUCT_0:def 5;
reconsider a2 =
a1 as
Element of
G by GROUP_2:42;
A16:
h2 = h . a2
by A14, FUNCT_1:49;
then A17:
(g * h2) * H2 =
((h . a) * (h . a2)) * (h .: G2)
by A12, A3, Th24
.=
h .: ((a * a2) * G2)
by Th23
;
A18:
(h2 * g) * H2 =
((h . a2) * (h . a)) * (h .: G2)
by A12, A16, A3, Th24
.=
h .: ((a2 * a) * G2)
by Th23
;
A19:
[.G1,((Omega). G).] is
strict Subgroup of
G2
by A1, A2, Th19;
[.a2,a.] in [.G1,((Omega). G).]
by A13, A15, GROUP_5:65;
then
[.a2,a.] in G2
by A19, GROUP_2:40;
then (a * a2) * G2 =
(a * a2) * ([.a2,a.] * G2)
by GROUP_2:113
.=
(a * a2) * ((((a2 ") * (a ")) * (a2 * a)) * G2)
by GROUP_5:16
.=
((a * a2) * (((a2 ") * (a ")) * (a2 * a))) * G2
by GROUP_2:32
.=
(((a * a2) * ((a2 ") * (a "))) * (a2 * a)) * G2
by GROUP_1:def 3
.=
((a * (a2 * ((a2 ") * (a ")))) * (a2 * a)) * G2
by GROUP_1:def 3
.=
((a * ((a2 * (a2 ")) * (a "))) * (a2 * a)) * G2
by GROUP_1:def 3
.=
((a * ((1_ G) * (a "))) * (a2 * a)) * G2
by GROUP_1:def 5
.=
((a * (a ")) * (a2 * a)) * G2
by GROUP_1:def 4
.=
((1_ G) * (a2 * a)) * G2
by GROUP_1:def 5
.=
(a2 * a) * G2
by GROUP_1:def 4
;
hence
S * T = T * S
by A10, A11, A17, A18;
verum
end;
hence
T in center ((Image h) ./. H2)
by GROUP_5:77;
verum
end;
hence
H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2)
by GROUP_2:58; verum