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 Lm33;
now for H being strict Subgroup of H1 st H = multMagma(# the carrier of A, the multF of A #) holds
H is normal reconsider N9 =
multMagma(# the
carrier of
N, the
multF of
N #) as
normal Subgroup of
G by Lm6;
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 for b being Element of H1 holds b * H c= H * blet b be
Element of
H1;
b * H c= H * bthus
b * H c= H * b
verumproof
let x be
object ;
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
H1 such that A2:
x = b * a
and A3:
a in H
by GROUP_2:103;
reconsider a9 =
a,
b9 =
b as
Element of
G by Th2;
reconsider x9 =
x as
Element of
H1 by A2;
A4:
b9 " = b "
by Th6;
a in the
carrier of
A
by A1, A3, STRUCT_0:def 5;
then
a in (carr H1) /\ (carr N)
by Def25;
then
a in carr N9
by XBOOLE_0:def 4;
then A5:
a in N9
by STRUCT_0:def 5;
x = b9 * a9
by A2, Th3;
then A6:
x in b9 * N9
by A5, GROUP_2:103;
b9 * N9 c= N9 * b9
by GROUP_3:118;
then consider b1 being
Element of
G such that A7:
x = b1 * b9
and A8:
b1 in N9
by A6, GROUP_2:104;
reconsider x99 =
x as
Element of
G by A7;
b1 = x99 * (b9 ")
by A7, GROUP_1:14;
then A9:
b1 = x9 * (b ")
by A4, Th3;
then reconsider b19 =
b1 as
Element of
H1 ;
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
b19 in the
carrier of
A
by Def25;
then A10:
b19 in H
by A1, STRUCT_0:def 5;
b19 * b = x
by A7, Th3;
hence
x in H * b
by A10, GROUP_2:104;
verum
end; end; hence
H is
normal
by GROUP_3:118;
verum end;
hence
H1 /\ N is
normal StableSubgroup of
H1
by Def10;
verum
end;
hence
N /\ H1 is normal StableSubgroup of H1
; verum