let G be strict Group; :: 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 GROUP_2:62; :: 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_3:def 13 :: thesis: H |^ a = multMagma(# the carrier of H, the multF 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 = multMagma(# the carrier of H, the multF of H #) ; :: thesis: verum
end;
hence H is normal Subgroup of G ; :: thesis: verum