let G be Group; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
thus ( H is normal Subgroup of G implies for a being Element of G holds H * a c= a * H ) by Th117; :: thesis: ( ( for a being Element of G holds H * a c= a * H ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds H * a c= a * H ; :: thesis: H is normal Subgroup of G
now :: thesis: for a being Element of G holds a * H c= H * a
let a be Element of G; :: thesis: a * H c= H * a
H * (a ") c= (a ") * H by A1;
then a * (H * (a ")) c= a * ((a ") * H) by Th4;
then a * (H * (a ")) c= (a * (a ")) * H by GROUP_2:105;
then a * (H * (a ")) c= (1_ G) * H by GROUP_1:def 5;
then a * (H * (a ")) c= carr H by GROUP_2:109;
then (a * H) * (a ") c= carr H by GROUP_2:106;
then ((a * H) * (a ")) * a c= (carr H) * a by Th4;
then (a * H) * ((a ") * a) c= H * a by GROUP_2:34;
then (a * H) * (1_ G) c= H * a by GROUP_1:def 5;
hence a * H c= H * a by GROUP_2:37; :: thesis: verum
end;
then for a being Element of G holds a * H = H * a by A1;
hence H is normal Subgroup of G by Th117; :: thesis: verum