let G be strict addGroup; :: thesis: for H being strict Subgroup of G holds
( H is normal Subgroup of G iff Normalizer H = G )
let H be strict Subgroup of G; :: thesis: ( H is normal Subgroup of G iff Normalizer H = G )
thus ( H is normal Subgroup of G implies Normalizer H = G ) :: thesis: ( Normalizer H = G implies H is normal Subgroup of G )

proof

assume A1: H is normal Subgroup of G ; :: thesis: Normalizer H = G

now :: thesis: for a being Element of G holds a in Normalizer H

let a be Element of G; :: thesis: a in Normalizer H
H * a = H by A1, Def13;
hence a in Normalizer H by Th134; :: thesis: verum

end;

hence Normalizer H = G by Th62; :: thesis: verum

end;

assume A2: Normalizer H = G ; :: thesis: H is normal Subgroup of G
H is normal

proof

let a be Element of G; :: according to GROUP_1A:def 41 :: thesis: H * a = addMagma(# the carrier of H, the addF of H #)
a in Normalizer H by A2;
then ex b being Element of G st
( b = a & H * b = H ) by Th134;
hence H * a = addMagma(# the carrier of H, the addF of H #) ; :: thesis: verum

end;

hence H is normal Subgroup of G ; :: thesis: verum