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