let G be Group; :: thesis: for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. (N,M `*` ) is normal Subgroup of G ./. M
let N, M be strict normal Subgroup of G; :: thesis: ( M is Subgroup of N implies N ./. (N,M `*` ) is normal Subgroup of G ./. M )
assume A1:
M is Subgroup of N
; :: thesis: N ./. (N,M `*` ) is normal Subgroup of G ./. M
then A2:
N,M `*` = M
by Def1;
reconsider J = N ./. (N,M `*` ) as Subgroup of G ./. M by A1, Th34;
reconsider I = M as normal Subgroup of N by A2;
now let S be
Element of
(G ./. M);
:: thesis: S * J c= J * Sthus
S * J c= J * S
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in S * J or x in J * S )
assume
x in S * J
;
:: thesis: x in J * S
then consider T being
Element of
(G ./. M) such that A3:
x = S * T
and A4:
T in J
by GROUP_2:125;
consider a being
Element of
G such that A5:
(
S = a * M &
S = M * a )
by Th15;
consider c being
Element of
N such that A6:
(
T = c * I &
T = I * c )
by A2, A4, Th28;
reconsider d =
c as
Element of
G by GROUP_2:51;
set e =
a * (d * (a " ));
A7:
c in N
by STRUCT_0:def 5;
a * (d * (a " )) = d |^ (a " )
by Th4;
then
a * (d * (a " )) in N
by A7, GROUP_5:3;
then reconsider f =
a * (d * (a " )) as
Element of
N by STRUCT_0:def 5;
reconsider V =
I * f as
Element of
J by A2, Th16;
A8:
V in J
by STRUCT_0:def 5;
reconsider V =
V as
Element of
(G ./. M) by GROUP_2:51;
A9:
(
@ S = S &
@ T = T &
c * I = d * M &
M * d = I * c &
M * (a * (d * (a " ))) = I * f &
@ V = V )
by Th2;
then x =
(M * a) * (M * d)
by A3, A5, A6, Def4
.=
(M * a) * ((M * d) * (1_ G))
by GROUP_2:43
.=
(M * a) * ((M * d) * ((a " ) * a))
by GROUP_1:def 6
.=
(M * a) * (M * (d * ((a " ) * a)))
by GROUP_2:129
.=
((M * a) * M) * (d * ((a " ) * a))
by GROUP_3:12
.=
(M * (a * M)) * (d * ((a " ) * a))
by GROUP_3:15
.=
(M * (M * a)) * (d * ((a " ) * a))
by GROUP_3:140
.=
M * ((M * a) * (d * ((a " ) * a)))
by GROUP_2:118
.=
M * (M * (a * (d * ((a " ) * a))))
by GROUP_2:129
.=
M * (M * (a * ((d * (a " )) * a)))
by GROUP_1:def 4
.=
M * (M * ((a * (d * (a " ))) * a))
by GROUP_1:def 4
.=
M * ((M * (a * (d * (a " )))) * a)
by GROUP_2:129
.=
M * (((a * (d * (a " ))) * M) * a)
by GROUP_3:140
.=
M * ((a * (d * (a " ))) * (M * a))
by GROUP_2:128
.=
(M * (a * (d * (a " )))) * (M * a)
by GROUP_3:13
.=
V * S
by A5, A9, Def4
;
hence
x in J * S
by A8, GROUP_2:126;
:: thesis: verum
end; end;
hence
N ./. (N,M `*` ) is normal Subgroup of G ./. M
by GROUP_3:141; :: thesis: verum