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