let G be Group; for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
let B be Subgroup of G; for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
let N be normal Subgroup of G; ( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
thus
B /\ N is normal Subgroup of B
N /\ B is normal Subgroup of Bproof
reconsider A =
B /\ N as
Subgroup of
B by GROUP_2:88;
now for b being Element of B holds b * A c= A * blet b be
Element of
B;
b * A c= A * bthus
b * A c= A * b
verumproof
let x be
object ;
TARSKI:def 3 ( not x in b * A or x in A * b )
assume
x in b * A
;
x in A * b
then consider a being
Element of
B such that A1:
x = b * a
and A2:
a in A
by GROUP_2:103;
reconsider a9 =
a,
b9 =
b as
Element of
G by GROUP_2:42;
(
a in N &
x = b9 * a9 )
by A1, A2, GROUP_2:43, GROUP_2:82;
then A3:
x in b9 * N
by GROUP_2:103;
reconsider x9 =
x as
Element of
B by A1;
A4:
b9 " = b "
by GROUP_2:48;
b9 * N c= N * b9
by GROUP_3:118;
then consider b1 being
Element of
G such that A5:
x = b1 * b9
and A6:
b1 in N
by A3, GROUP_2:104;
reconsider x99 =
x as
Element of
G by A5;
b1 = x99 * (b9 ")
by A5, GROUP_1:14;
then A7:
b1 = x9 * (b ")
by A4, GROUP_2:43;
then reconsider b19 =
b1 as
Element of
B ;
b1 in B
by A7;
then A8:
b19 in A
by A6, GROUP_2:82;
b19 * b = x
by A5, GROUP_2:43;
hence
x in A * b
by A8, GROUP_2:104;
verum
end; end;
hence
B /\ N is
normal Subgroup of
B
by GROUP_3:118;
verum
end;
hence
N /\ B is normal Subgroup of B
; verum