let G be Group; :: thesis: for A being non empty Subset of G holds the carrier of (Centralizer A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) }
let A be non empty Subset of G; :: thesis: the carrier of (Centralizer A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) }
defpred S₁[ strict Subgroup of G] means ex a being Element of G st
( a in A & $1 = Normalizer a );
set Fam = { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } ;
A1: { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } <> {}

proof

consider a being object such that
B1: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of G by B1;
consider H being strict Subgroup of G such that
B2: H = Normalizer a ;
carr H in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } by B1, B2;
hence { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } <> {} ; :: thesis: verum

end;

for x being object st x in the carrier of (Centralizer A) holds
x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) }

proof

let x be object ; :: thesis: ( x in the carrier of (Centralizer A) implies x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } )
assume B1: x in the carrier of (Centralizer A) ; :: thesis: x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) }
then x in Centralizer A ;
then x in G by GROUP_2:40;
then reconsider g = x as Element of G ;
for X being set st X in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } holds
x in X

proof

let X be set ; :: thesis: ( X in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } implies x in X )
assume X in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } ; :: thesis: x in X
then consider B being Subset of G such that
C1: B = X and
C2: ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) ;
consider H being strict Subgroup of G, a being Element of G such that
C3: ( B = the carrier of H & a in A & H = Normalizer a ) by C2;
C4: a |^ g = (g ") * (a * g) by GROUP_1:def 3
.= (g ") * (g * a) by B1, C3, Th57
.= ((g ") * g) * a by GROUP_1:def 3
.= (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
{a} |^ g = {(a |^ g)} by GROUP_3:37
.= {a} by C4 ;
then g in Normalizer a by GROUP_3:129;
hence x in X by C1, C3; :: thesis: verum

end;

hence x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } by A1, SETFAM_1:def 1; :: thesis: verum

end;

then A2: the carrier of (Centralizer A) c= meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } ;
for x being object st x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } holds
x in the carrier of (Centralizer A)

proof

let x be object ; :: thesis: ( x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } implies x in the carrier of (Centralizer A) )
assume B1: x in meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } ; :: thesis: x in the carrier of (Centralizer A)
B2: ex H being strict Subgroup of G st S₁[H]

proof

consider X being object such that
C1: X in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } by A1, XBOOLE_0:def 1;
consider B being Subset of G such that
C2: ( B = X & ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) ) by C1;
thus ex H being strict Subgroup of G st S₁[H] by C2; :: thesis: verum

end;

consider K being strict Subgroup of G such that
B3: the carrier of K = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } from GROUP_4:sch 1(B2);
reconsider g = x as Element of G by B1, B3, GROUP_2:42;
B4: for a being Element of G st a in A holds
g in Normalizer a

proof

let a be Element of G; :: thesis: ( a in A implies g in Normalizer a )
assume a in A ; :: thesis: g in Normalizer a
then carr (Normalizer a) in { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } ;
hence g in Normalizer a by B1, SETFAM_1:def 1; :: thesis: verum

end;

for a being Element of G st a in A holds
g * a = a * g

proof

let a be Element of G; :: thesis: ( a in A implies g * a = a * g )
assume a in A ; :: thesis: g * a = a * g
then g in Normalizer a by B4;
then consider h being Element of G such that
C1: ( g = h & a |^ h = a ) by Th64;
C2: a = ((g ") * a) * g by C1
.= (g ") * (a * g) by GROUP_1:def 3 ;
g * a = g * ((g ") * (a * g)) by C2
.= (g * (g ")) * (a * g) by GROUP_1:def 3
.= (1_ G) * (a * g) by GROUP_1:def 5
.= a * g by GROUP_1:def 4 ;
hence g * a = a * g ; :: thesis: verum

end;

then g is Element of (Centralizer A) by Th57;
hence x in the carrier of (Centralizer A) ; :: thesis: verum

end;

then meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & S₁[H] ) } c= the carrier of (Centralizer A) ;
hence the carrier of (Centralizer A) = meet { B where B is Subset of G : ex H being strict Subgroup of G st
( B = the carrier of H & ex a being Element of G st
( a in A & H = Normalizer a ) ) } by A2, XBOOLE_0:def 10; :: thesis: verum