let G be addGroup; :: thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H * a )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds H is Subgroup of H * a )
thus ( H is normal Subgroup of G implies for a being Element of G holds H is Subgroup of H * a ) :: thesis: ( ( for a being Element of G holds H is Subgroup of H * a ) implies H is normal Subgroup of G )
proof
assume A1: H is normal Subgroup of G ; :: thesis: for a being Element of G holds H is Subgroup of H * a
let a be Element of G; :: thesis: H is Subgroup of H * a
H * a = addMagma(# the carrier of H, the addF of H #) by A1, Def13;
hence H is Subgroup of H * a by ThA54; :: thesis: verum
end;
assume A2: for a being Element of G holds H is Subgroup of H * a ; :: thesis: H is normal Subgroup of G
now :: thesis: for a being Element of G holds H + a c= a + H
let a be Element of G; :: thesis: H + a c= a + H
A3: (H * (- a)) + a = (((- (- a)) + H) + (- a)) + a by ThB59
.= ((- (- a)) + H) + ((- a) + a) by ThB34
.= ((- (- a)) + H) + (0_ G) by Def5
.= a + H by Th37 ;
H is Subgroup of H * (- a) by A2;
hence H + a c= a + H by A3, ThB6; :: thesis: verum
end;
hence H is normal Subgroup of G by ThB119; :: thesis: verum