let O be set ; :: thesis: for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
let G be GroupWithOperators of O; :: thesis: for N being normal StableSubgroup of G
for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
let N be normal StableSubgroup of G; :: thesis: for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
let H1 be StableSubgroup of G; :: thesis: ( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )
thus
H1 /\ N is normal StableSubgroup of H1
:: thesis: N /\ H1 is normal StableSubgroup of H1proof
reconsider A =
H1 /\ N as
StableSubgroup of
H1 by Lm34;
now let H be
strict Subgroup of
H1;
:: thesis: ( H = multMagma(# the carrier of A,the multF of A #) implies H is normal )assume A1:
H = multMagma(# the
carrier of
A,the
multF of
A #)
;
:: thesis: H is normalreconsider N' =
multMagma(# the
carrier of
N,the
multF of
N #) as
normal Subgroup of
G by Lm7;
now let b be
Element of
H1;
:: thesis: b * H c= H * bthus
b * H c= H * b
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in b * H or x in H * b )
assume
x in b * H
;
:: thesis: x in H * b
then consider a being
Element of
H1 such that A2:
x = b * a
and A3:
a in H
by GROUP_2:125;
a in the
carrier of
A
by A1, A3, STRUCT_0:def 5;
then
a in (carr H1) /\ (carr N)
by Def28;
then
a in carr N'
by XBOOLE_0:def 4;
then A4:
a in N'
by STRUCT_0:def 5;
reconsider a' =
a,
b' =
b as
Element of
G by Th2;
x = b' * a'
by A2, Th3;
then
(
x in b' * N' &
b' * N' c= N' * b' )
by A4, GROUP_2:125, GROUP_3:141;
then consider b1 being
Element of
G such that A5:
x = b1 * b'
and A6:
b1 in N'
by GROUP_2:126;
reconsider x' =
x as
Element of
H1 by A2;
reconsider x'' =
x as
Element of
G by A5;
A7:
b1 = x'' * (b' " )
by A5, GROUP_1:22;
A8:
b1 in the
carrier of
N
by A6, STRUCT_0:def 5;
b' " = b "
by Th6;
then A9:
b1 = x' * (b " )
by A7, Th3;
then A10:
b1 in (carr H1) /\ (carr N)
by A8, XBOOLE_0:def 4;
reconsider b1' =
b1 as
Element of
H1 by A9;
b1' in the
carrier of
A
by A10, Def28;
then A11:
b1' in H
by A1, STRUCT_0:def 5;
b1' * b = x
by A5, Th3;
hence
x in H * b
by A11, GROUP_2:126;
:: thesis: verum
end; end; hence
H is
normal
by GROUP_3:141;
:: thesis: verum end;
hence
H1 /\ N is
normal StableSubgroup of
H1
by Def10;
:: thesis: verum
end;
hence
N /\ H1 is normal StableSubgroup of H1
; :: thesis: verum