let G be strict Group; :: thesis: for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds

b |^ a in H ) holds

H is normal

let H be Subgroup of G; :: thesis: ( ( for a, b being Element of G st b is Element of H holds

b |^ a in H ) implies H is normal )

assume A1: for a, b being Element of G st b is Element of H holds

b |^ a in H ; :: thesis: H is normal

b |^ a in H ) holds

H is normal

let H be Subgroup of G; :: thesis: ( ( for a, b being Element of G st b is Element of H holds

b |^ a in H ) implies H is normal )

assume A1: for a, b being Element of G st b is Element of H holds

b |^ a in H ; :: thesis: H is normal

now :: thesis: for a being Element of G holds H * a c= a * H

hence
H is normal
by GROUP_3:119; :: thesis: verumlet a be Element of G; :: thesis: H * a c= a * H

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

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

proof

set A = carr H;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in H * a or q in a * H )

assume q in H * a ; :: thesis: q in a * H

then consider b being Element of G such that

A2: q = b * a and

A3: b in H by GROUP_2:104;

b is Element of H by A3, STRUCT_0:def 5;

then b |^ a in H by A1;

then b |^ a in carr H by STRUCT_0:def 5;

then a * (((a ") * b) * a) in a * (carr H) by GROUP_2:27;

then a * ((a ") * (b * a)) in a * (carr H) by GROUP_1:def 3;

then (a * (a ")) * (b * a) in a * (carr H) by GROUP_1:def 3;

then ((a * (a ")) * b) * a in a * (carr H) by GROUP_1:def 3;

then ((1_ G) * b) * a in a * (carr H) by GROUP_1:def 5;

hence q in a * H by A2, GROUP_1:def 4; :: thesis: verum

end;let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in H * a or q in a * H )

assume q in H * a ; :: thesis: q in a * H

then consider b being Element of G such that

A2: q = b * a and

A3: b in H by GROUP_2:104;

b is Element of H by A3, STRUCT_0:def 5;

then b |^ a in H by A1;

then b |^ a in carr H by STRUCT_0:def 5;

then a * (((a ") * b) * a) in a * (carr H) by GROUP_2:27;

then a * ((a ") * (b * a)) in a * (carr H) by GROUP_1:def 3;

then (a * (a ")) * (b * a) in a * (carr H) by GROUP_1:def 3;

then ((a * (a ")) * b) * a in a * (carr H) by GROUP_1:def 3;

then ((1_ G) * b) * a in a * (carr H) by GROUP_1:def 5;

hence q in a * H by A2, GROUP_1:def 4; :: thesis: verum