let G be Group; :: thesis: for H being Subgroup of G holds Centralizer H is strict Subgroup of Normalizer H
let H be Subgroup of G; :: thesis: Centralizer H is strict Subgroup of Normalizer H
set Z = Centralizer H;
for g being Element of G st g in Centralizer H holds
g in Normalizer H

proof

let g be Element of G; :: thesis: ( g in Centralizer H implies g in Normalizer H )
assume A1: g in Centralizer H ; :: thesis: g in Normalizer H
A2: for a being Element of G st a in H holds
a = ((g ") * a) * g

proof

let a be Element of G; :: thesis: ( a in H implies a = ((g ") * a) * g )
assume a in H ; :: thesis: a = ((g ") * a) * g
then (g ") * (a * g) = (g ") * (g * a) by A1, Th60
.= ((g ") * g) * a by GROUP_1:def 3
.= (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
hence a = ((g ") * a) * g by GROUP_1:def 3; :: thesis: verum

end;

for a being Element of G holds
( a in H iff a in H |^ g )

proof

let a be Element of G; :: thesis: ( a in H iff a in H |^ g )
thus ( a in H implies a in H |^ g ) :: thesis: ( a in H |^ g implies a in H )

proof

assume B1: a in H ; :: thesis: a in H |^ g
then a = a |^ g by A2;
hence a in H |^ g by B1, GROUP_3:58; :: thesis: verum

end;

thus ( a in H |^ g implies a in H ) :: thesis: verum

proof

assume a in H |^ g ; :: thesis: a in H
then consider h being Element of G such that
B1: ( a = h |^ g & h in H ) by GROUP_3:58;
thus a in H by A2, B1; :: thesis: verum

end;

end;

then multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of (H |^ g), the multF of (H |^ g) #) by GROUP_2:60;
then carr H = (carr H) |^ g by GROUP_3:def 6;
hence g in Normalizer H by GROUP_3:129; :: thesis: verum

end;

hence Centralizer H is strict Subgroup of Normalizer H by GROUP_2:58; :: thesis: verum