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:106;
now let b be
Element of ;
b * A c= A * bthus
b * A c= A * b
verumproof
let x be
set ;
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
such that A1:
x = b * a
and A2:
a in A
by GROUP_2:125;
reconsider a' =
a,
b' =
b as
Element of
by GROUP_2:51;
(
a in N &
x = b' * a' )
by A1, A2, GROUP_2:52, GROUP_2:99;
then A3:
x in b' * N
by GROUP_2:125;
reconsider x' =
x as
Element of
by A1;
A4:
b' " = b "
by GROUP_2:57;
b' * N c= N * b'
by GROUP_3:141;
then consider b1 being
Element of
such that A5:
x = b1 * b'
and A6:
b1 in N
by A3, GROUP_2:126;
reconsider x'' =
x as
Element of
by A5;
b1 = x'' * (b' " )
by A5, GROUP_1:22;
then A7:
b1 = x' * (b " )
by A4, GROUP_2:52;
then reconsider b1' =
b1 as
Element of ;
b1 in B
by A7, STRUCT_0:def 5;
then A8:
b1' in A
by A6, GROUP_2:99;
b1' * b = x
by A5, GROUP_2:52;
hence
x in A * b
by A8, GROUP_2:126;
verum
end; end;
hence
B /\ N is
normal Subgroup of
B
by GROUP_3:141;
verum
end;
hence
N /\ B is normal Subgroup of B
; verum