let G be Group; :: thesis: for H being Subgroup of G holds the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }
let H be Subgroup of G; :: thesis: the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }
set A = carr H;
set Car = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } ;
A1: the carrier of (Centralizer (carr H)) = { b where b is Element of G : for a being Element of G st a in carr H holds
b * a = a * b } by Def4;
for x being object st x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } holds
x in the carrier of (Centralizer H)

proof

let x be object ; :: thesis: ( x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } implies x in the carrier of (Centralizer H) )
assume B1: x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } ; :: thesis: x in the carrier of (Centralizer H)
ex b being Element of G st
( x = b & ( for a being Element of G st a in carr H holds
b * a = a * b ) )

proof

consider b being Element of G such that
B2: x = b and
B3: for a being Element of G st a in H holds
b * a = a * b by B1;
for a being Element of G st a in carr H holds
b * a = a * b

proof

let a be Element of G; :: thesis: ( a in carr H implies b * a = a * b )
assume a in carr H ; :: thesis: b * a = a * b
then a in H ;
hence b * a = a * b by B3; :: thesis: verum

end;

hence ex b being Element of G st
( x = b & ( for a being Element of G st a in carr H holds
b * a = a * b ) ) by B2; :: thesis: verum

end;

then x in the carrier of (Centralizer (carr H)) by A1;
hence x in the carrier of (Centralizer H) by Def5; :: thesis: verum

end;

then A3: { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } c= the carrier of (Centralizer H) ;
for x being object st x in the carrier of (Centralizer H) holds
x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }

proof

let x be object ; :: thesis: ( x in the carrier of (Centralizer H) implies x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } )
assume x in the carrier of (Centralizer H) ; :: thesis: x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b }
then B1: x in the carrier of (Centralizer (carr H)) by Def5;
ex b being Element of G st
( x = b & ( for a being Element of G st a in H holds
b * a = a * b ) )

proof

consider b being Element of G such that
Z1: ( x = b & ( for a being Element of G st a in carr H holds
b * a = a * b ) ) by A1, B1;
for a being Element of G st a in H holds
b * a = a * b by Z1;
hence ex b being Element of G st
( x = b & ( for a being Element of G st a in H holds
b * a = a * b ) ) by Z1; :: thesis: verum

end;

hence x in { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } ; :: thesis: verum

end;

then the carrier of (Centralizer H) c= { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } ;
hence the carrier of (Centralizer H) = { b where b is Element of G : for a being Element of G st a in H holds
b * a = a * b } by A3, XBOOLE_0:def 10; :: thesis: verum