let G be Group; :: thesis: for N being normal Subgroup of G holds Centralizer N is normal Subgroup of G
let N be normal Subgroup of G; :: thesis: Centralizer N is normal Subgroup of G
A1: for g, n being Element of G st n in N holds
n |^ g in N

proof

let g, n be Element of G; :: thesis: ( n in N implies n |^ g in N )
assume B1: n in N ; :: thesis: n |^ g in N
B2: multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of (N |^ g), the multF of (N |^ g) #) by GROUP_3:def 13;
n |^ g in N |^ g by B1, GROUP_3:58;
hence n |^ g in N by B2; :: thesis: verum

end;

A2: for g, x, n being Element of G st x in Centralizer N & n in N holds
(x |^ g) * n = n * (x |^ g)

proof

let g, x, n be Element of G; :: thesis: ( x in Centralizer N & n in N implies (x |^ g) * n = n * (x |^ g) )
assume B1: x in Centralizer N ; :: thesis: ( not n in N or (x |^ g) * n = n * (x |^ g) )
assume B2: n in N ; :: thesis: (x |^ g) * n = n * (x |^ g)
consider n2 being Element of G such that
B3: n2 = (g * n) * (g ") ;
B4: n2 = n |^ (g ") by B3;
then (x * n2) |^ g = (n2 * x) |^ g by B1, B2, A1, Th60
.= (n2 |^ g) * (x |^ g) by GROUP_3:23 ;
then (x |^ g) * (n2 |^ g) = (n2 |^ g) * (x |^ g) by GROUP_3:23
.= n * (x |^ g) by B4, GROUP_3:25 ;
hence (x |^ g) * n = n * (x |^ g) by B4, GROUP_3:25; :: thesis: verum

end;

A3: for g, z being Element of G st z in Centralizer N holds
z |^ g in Centralizer N

proof

let g, z be Element of G; :: thesis: ( z in Centralizer N implies z |^ g in Centralizer N )
assume z in Centralizer N ; :: thesis: z |^ g in Centralizer N
then for n being Element of G st n in N holds
(z |^ g) * n = n * (z |^ g) by A2;
then z |^ g is Element of (Centralizer N) by Th60;
hence z |^ g in Centralizer N ; :: thesis: verum

end;

for g being Element of G holds (Centralizer N) |^ g = Centralizer N

proof

let g be Element of G; :: thesis: (Centralizer N) |^ g = Centralizer N
for z being Element of G holds
( z in (Centralizer N) |^ g iff z in Centralizer N )

proof

let z be Element of G; :: thesis: ( z in (Centralizer N) |^ g iff z in Centralizer N )

hereby :: thesis: ( z in Centralizer N implies z in (Centralizer N) |^ g )

assume z in (Centralizer N) |^ g ; :: thesis: z in Centralizer N
then z |^ (g ") in ((Centralizer N) |^ g) |^ (g ") by GROUP_3:58;
then z |^ (g ") in Centralizer N by GROUP_3:62;
then (z |^ (g ")) |^ g in Centralizer N by A3;
hence z in Centralizer N by GROUP_3:25; :: thesis: verum

end;

assume z in Centralizer N ; :: thesis: z in (Centralizer N) |^ g
then (z |^ (g ")) |^ g in (Centralizer N) |^ g by A3, GROUP_3:58;
hence z in (Centralizer N) |^ g by GROUP_3:25; :: thesis: verum

end;

hence (Centralizer N) |^ g = Centralizer N ; :: thesis: verum

end;

hence Centralizer N is normal Subgroup of G by GROUP_3:def 13; :: thesis: verum