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 H1

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 H1

proof

hence
N /\ H1 is normal StableSubgroup of H1
; :: thesis: verum
reconsider A = H1 /\ N as StableSubgroup of H1 by Lm33;

end;now :: thesis: for H being strict Subgroup of H1 st H = multMagma(# the carrier of A, the multF of A #) holds

H is normal

hence
H1 /\ N is normal StableSubgroup of H1
by Def10; :: thesis: verumH 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; :: 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 normal

end;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 normal

now :: thesis: for b being Element of H1 holds b * H c= H * b

hence
H is normal
by GROUP_3:118; :: thesis: verumlet b be Element of H1; :: thesis: b * H c= H * b

thus b * H c= H * b :: thesis: verum

end;thus b * H c= H * b :: thesis: verum

proof

let x be object ; :: 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: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; :: thesis: verum

end;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: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; :: thesis: verum