let G be Group; :: thesis: for H being Subgroup of G holds Centralizer H is strict normal Subgroup of Normalizer H
let H be Subgroup of G; :: thesis: Centralizer H is strict normal Subgroup of Normalizer H
Centralizer H is normal Subgroup of Normalizer H

proof

reconsider Z = Centralizer H as strict Subgroup of Normalizer H by Lm8;
set N = Normalizer H;
B60: for z being Element of (Normalizer H) holds
( ( for n being Element of (Normalizer H) st n in H holds
z * n = n * z ) iff z is Element of Z )

proof

let z be Element of (Normalizer H); :: thesis: ( ( for n being Element of (Normalizer H) st n in H holds
z * n = n * z ) iff z is Element of Z )
reconsider z1 = z as Element of G by GROUP_2:42;
C1: ( z is Element of Z implies for n being Element of (Normalizer H) st n in H holds
z * n = n * z )

proof

assume D1: z is Element of Z ; :: thesis: for n being Element of (Normalizer H) st n in H holds
z * n = n * z
let n be Element of (Normalizer H); :: thesis: ( n in H implies z * n = n * z )
assume D2: n in H ; :: thesis: z * n = n * z
reconsider n1 = n as Element of G by GROUP_2:42;
z1 * n1 = n1 * z1 by D1, D2, Th60
.= n * z by GROUP_2:43 ;
hence z * n = n * z by GROUP_2:43; :: thesis: verum

end;

( z is not Element of Z implies ex n being Element of (Normalizer H) st
( n in H & not z * n = n * z ) )

proof

assume z is not Element of Z ; :: thesis: ex n being Element of (Normalizer H) st
( n in H & not z * n = n * z )
then consider g being Element of G such that
D1: ( g in H & g * z1 <> z1 * g ) by Th60;
H is Subgroup of Normalizer H by Th80;
then g in Normalizer H by D1, GROUP_2:41;
then reconsider n = g as Element of (Normalizer H) ;
D2: g * z1 = n * z by GROUP_2:43;
take n ; :: thesis: ( n in H & not z * n = n * z )
thus ( n in H & not z * n = n * z ) by D1, D2, GROUP_2:43; :: thesis: verum

end;

hence ( ( for n being Element of (Normalizer H) st n in H holds
z * n = n * z ) implies z is Element of Z ) ; :: thesis: ( z is Element of Z implies for n being Element of (Normalizer H) st n in H holds
z * n = n * z )
thus ( z is Element of Z implies for n being Element of (Normalizer H) st n in H holds
z * n = n * z ) by C1; :: thesis: verum

end;

B1: for z, n, h being Element of (Normalizer H) st z in Z & n in Normalizer H & h in H holds
h |^ (z |^ n) = h

proof

let z, n, h be Element of (Normalizer H); :: thesis: ( z in Z & n in Normalizer H & h in H implies h |^ (z |^ n) = h )
assume C1: z in Z ; :: thesis: ( not n in Normalizer H or not h in H or h |^ (z |^ n) = h )
assume n in Normalizer H ; :: thesis: ( not h in H or h |^ (z |^ n) = h )
assume C2: h in H ; :: thesis: h |^ (z |^ n) = h
C3: h |^ (z |^ n) = (((z ") |^ n) * h) * (z |^ n) by GROUP_3:26
.= ((((n ") * (z ")) * n) * h) * ((n ") * (z * n)) by GROUP_1:def 3
.= (((n ") * (z ")) * n) * (h * ((n ") * (z * n))) by GROUP_1:def 3
.= ((n ") * (z ")) * (n * (h * ((n ") * (z * n)))) by GROUP_1:def 3
.= ((n ") * (z ")) * ((n * h) * ((n ") * (z * n))) by GROUP_1:def 3
.= ((n ") * (z ")) * (((n * h) * (n ")) * (z * n)) by GROUP_1:def 3
.= (((n ") * (z ")) * ((n * h) * (n "))) * (z * n) by GROUP_1:def 3
.= (((n ") * (z ")) * ((n * h) * (n "))) * (z * n) ;
C4: for a, b being Element of G st a in Normalizer H & b in H & b in Normalizer H holds
( (a * b) * (a ") in H & (a * b) * (a ") in Normalizer H )

proof

let a, b be Element of G; :: thesis: ( a in Normalizer H & b in H & b in Normalizer H implies ( (a * b) * (a ") in H & (a * b) * (a ") in Normalizer H ) )
assume D1: a in Normalizer H ; :: thesis: ( not b in H or not b in Normalizer H or ( (a * b) * (a ") in H & (a * b) * (a ") in Normalizer H ) )
assume D2: b in H ; :: thesis: ( not b in Normalizer H or ( (a * b) * (a ") in H & (a * b) * (a ") in Normalizer H ) )
assume b in Normalizer H ; :: thesis: ( (a * b) * (a ") in H & (a * b) * (a ") in Normalizer H )
then D4: a * b in Normalizer H by D1, GROUP_2:50;
D5: ( a " in Normalizer H & b in H ) by D1, D2, GROUP_2:51;
then b |^ (a ") in H by Th79;
hence (a * b) * (a ") in H ; :: thesis: (a * b) * (a ") in Normalizer H
thus (a * b) * (a ") in Normalizer H by D4, D5, GROUP_2:50; :: thesis: verum

end;

(n * h) * (n ") in H

proof

reconsider h1 = h, n1 = n as Element of G by GROUP_2:42;
n1 " = n " by GROUP_2:48;
then h1 * (n1 ") = h * (n ") by GROUP_2:43;
then n1 * (h1 * (n1 ")) = n * (h * (n ")) by GROUP_2:43
.= (n * h) * (n ") by GROUP_1:def 3 ;
then D1: (n1 * h1) * (n1 ") = (n * h) * (n ") by GROUP_1:def 3;
( h1 in Normalizer H & n1 in Normalizer H & h1 in H ) by C2;
hence (n * h) * (n ") in H by C4, D1; :: thesis: verum

end;

then consider h2 being Element of (Normalizer H) such that
C5: ( (n * h) * (n ") = h2 & h2 in H ) ;
z * h2 = h2 * z by B60, C1, C5;
then ((z ") * z) * h2 = (z ") * (h2 * z) by GROUP_1:def 3
.= ((z ") * h2) * z by GROUP_1:def 3 ;
then ((z ") * h2) * z = (1_ (Normalizer H)) * h2 by GROUP_1:def 5
.= h2 by GROUP_1:def 4 ;
then C6: h2 * (z ") = ((z ") * h2) * (z * (z ")) by GROUP_1:def 3
.= ((z ") * h2) * (1_ (Normalizer H)) by GROUP_1:def 5
.= (z ") * h2 by GROUP_1:def 4 ;
h |^ (z |^ n) = (((n ") * (z ")) * ((n * h) * (n "))) * (z * n) by C3
.= (((n ") * (z ")) * h2) * (z * n) by C5
.= ((n ") * (z ")) * (h2 * (z * n)) by GROUP_1:def 3
.= (n ") * ((z ") * (h2 * (z * n))) by GROUP_1:def 3
.= (n ") * (((z ") * h2) * (z * n)) by GROUP_1:def 3
.= (n ") * ((h2 * (z ")) * (z * n)) by C6
.= (n ") * (h2 * ((z ") * (z * n))) by GROUP_1:def 3
.= (n ") * (h2 * (((z ") * z) * n)) by GROUP_1:def 3
.= (n ") * (h2 * ((1_ (Normalizer H)) * n)) by GROUP_1:def 5
.= (n ") * (h2 * n) by GROUP_1:def 4
.= ((n ") * h2) * n by GROUP_1:def 3
.= ((n * h) * (n ")) |^ n by C5
.= (h |^ (n ")) |^ n
.= h by GROUP_3:25 ;
hence h |^ (z |^ n) = h ; :: thesis: verum

end;

B2: for z, n, h being Element of (Normalizer H) st z in Z & h in H holds
(z |^ n) * h = h * (z |^ n)

proof

let z, n, h be Element of (Normalizer H); :: thesis: ( z in Z & h in H implies (z |^ n) * h = h * (z |^ n) )
assume C1: z in Z ; :: thesis: ( not h in H or (z |^ n) * h = h * (z |^ n) )
assume C2: h in H ; :: thesis: (z |^ n) * h = h * (z |^ n)
n in Normalizer H ;
then h |^ (z |^ n) = h by C1, C2, B1;
hence (z |^ n) * h = h * (z |^ n) by GROUP_3:22; :: thesis: verum

end;

B3: for n, z being Element of (Normalizer H) st z in Z holds
z |^ n in Z

proof

let n, z be Element of (Normalizer H); :: thesis: ( z in Z implies z |^ n in Z )
assume C1: z in Z ; :: thesis: z |^ n in Z
set g = z |^ n;
for h being Element of (Normalizer H) st h in H holds
(z |^ n) * h = h * (z |^ n) by C1, B2;
then z |^ n is Element of Z by B60;
hence z |^ n in Z ; :: thesis: verum

end;

for n being Element of (Normalizer H) holds Z is Subgroup of Z |^ n

proof

let n be Element of (Normalizer H); :: thesis: Z is Subgroup of Z |^ n
for z being Element of (Normalizer H) st z in Z holds
z in Z |^ n

proof

let z be Element of (Normalizer H); :: thesis: ( z in Z implies z in Z |^ n )
assume z in Z ; :: thesis: z in Z |^ n
then (z |^ (n ")) |^ n in Z |^ n by B3, GROUP_3:58;
hence z in Z |^ n by GROUP_3:25; :: thesis: verum

end;

hence Z is Subgroup of Z |^ n by GROUP_2:58; :: thesis: verum

end;

hence Centralizer H is normal Subgroup of Normalizer H by GROUP_3:121; :: thesis: verum

end;

hence Centralizer H is strict normal Subgroup of Normalizer H ; :: thesis: verum