let G, H be strict Group; for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let h be Homomorphism of G,H; for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let A, B be strict Subgroup of G; ( A is strict normal Subgroup of B implies h .: A is strict normal Subgroup of h .: B )
assume
A is strict normal Subgroup of B
; h .: A is strict normal Subgroup of h .: B
then reconsider A1 = A as strict normal Subgroup of B ;
reconsider C = h .: A1 as strict Subgroup of h .: B by Th12;
for b2 being Element of (h .: B) holds b2 * C c= C * b2
proof
let b2 be
Element of
(h .: B);
b2 * C c= C * b2
A1:
b2 in h .: B
by STRUCT_0:def 5;
now for x being object st x in b2 * C holds
x in C * b2consider b1 being
Element of
B such that A2:
b2 = (h | B) . b1
by A1, GROUP_6:45;
reconsider b1 =
b1 as
Element of
G by GROUP_2:42;
A3:
b2 = h . b1
by A2, FUNCT_1:49;
reconsider b =
b1 as
Element of
B ;
let x be
object ;
( x in b2 * C implies x in C * b2 )assume
x in b2 * C
;
x in C * b2then consider g being
Element of
(h .: B) such that A4:
x = b2 * g
and A5:
g in C
by GROUP_2:103;
consider g1 being
Element of
A1 such that A6:
g = (h | A1) . g1
by A5, GROUP_6:45;
reconsider g1 =
g1 as
Element of
G by GROUP_2:42;
g = h . g1
by A6, FUNCT_1:49;
then A7:
x =
(h . b1) * (h . g1)
by A3, A4, GROUP_2:43
.=
h . (b1 * g1)
by GROUP_6:def 6
;
g1 in A1
by STRUCT_0:def 5;
then A8:
b1 * g1 in b1 * A1
by GROUP_2:103;
A9:
h .: (A1 * b1) = (h .: A1) * (h . b1)
by Th13;
b1 * A1 =
b * A1
by GROUP_6:2
.=
A1 * b
by GROUP_3:117
.=
A1 * b1
by GROUP_6:2
;
then
x in h .: (A1 * b1)
by A7, A8, FUNCT_2:35;
hence
x in C * b2
by A3, A9, GROUP_6:2;
verum end;
hence
b2 * C c= C * b2
;
verum
end;
hence
h .: A is strict normal Subgroup of h .: B
by GROUP_3:118; verum