let G be finite Group; :: thesis: for a being Element of G
for x being Element of con_class a holds card ((a -con_map ) " {x}) = card (Centralizer a)
let a be Element of G; :: thesis: for x being Element of con_class a holds card ((a -con_map ) " {x}) = card (Centralizer a)
let x be Element of con_class a; :: thesis: card ((a -con_map ) " {x}) = card (Centralizer a)
ex b being Element of G st
( b = x & a,b are_conjugated ) by GROUP_3:95;
then consider d being Element of G such that
A1: x = a |^ d by GROUP_3:88;
reconsider Cad = (Centralizer a) * d as Subset of G ;
A2: ex B, C being finite set st
( B = d * (Centralizer a) & C = Cad & card (Centralizer a) = card B & card (Centralizer a) = card C ) by GROUP_2:156;
for g being set holds
( g in (a -con_map ) " {x} iff g in Cad )

proof

let g be set ; :: thesis: ( g in (a -con_map ) " {x} iff g in Cad )

A3: now

assume A4: g in (a -con_map ) " {x} ; :: thesis: g in Cad
then (a -con_map ) . g in {x} by FUNCT_1:def 13;
then A5: (a -con_map ) . g = x by TARSKI:def 1;
reconsider y = g as Element of G by A4;
A6: (a -con_map ) . g = a |^ y by Def2;
A7: y * (((d " ) * a) * d) = (y * ((d " ) * a)) * d by GROUP_1:def 4
.= ((y * (d " )) * a) * d by GROUP_1:def 4 ;
y * (((y " ) * a) * y) = (y * ((y " ) * a)) * y by GROUP_1:def 4
.= a * y by GROUP_3:1 ;
then (((y * (d " )) * a) * d) * (d " ) = a * (y * (d " )) by A1, A5, A6, A7, GROUP_1:def 4;
then (y * (d " )) * a = a * (y * (d " )) by GROUP_3:1;
then y * (d " ) is Element of (Centralizer a) by Th8;
then consider z being Element of G such that
A8: z in the carrier of (Centralizer a) and
A9: y * (d " ) = z ;
A10: z in Centralizer a by A8, STRUCT_0:def 5;
reconsider z = z as Element of G ;
y = z * d by A9, GROUP_3:1;
hence g in Cad by A10, GROUP_2:126; :: thesis: verum

end;

now

assume g in Cad ; :: thesis: g in (a -con_map ) " {x}
then consider z being Element of G such that
A11: g = z * d and
A12: z in Centralizer a by GROUP_2:126;
reconsider y = g as Element of G by A11;
y * (d " ) = z by A11, GROUP_3:1;
then y * (d " ) in carr (Centralizer a) by A12, STRUCT_0:def 5;
then (y * (d " )) * a = a * (y * (d " )) by Th8;
then ((y * (d " )) * a) * d = a * ((y * (d " )) * d) by GROUP_1:def 4;
then ((y * (d " )) * a) * d = a * y by GROUP_3:1;
then (y * (d " )) * (a * d) = a * y by GROUP_1:def 4;
then (y " ) * ((y * (d " )) * (a * d)) = ((y " ) * a) * y by GROUP_1:def 4;
then ((y " ) * (y * (d " ))) * (a * d) = ((y " ) * a) * y by GROUP_1:def 4;
then (d " ) * (a * d) = ((y " ) * a) * y by GROUP_3:1;
then x = a |^ y by A1, GROUP_1:def 4;
then (a -con_map ) . y = x by Def2;
then A13: (a -con_map ) . y in {x} by TARSKI:def 1;
dom (a -con_map ) = the carrier of G by FUNCT_2:def 1;
hence g in (a -con_map ) " {x} by A13, FUNCT_1:def 13; :: thesis: verum

end;

hence ( g in (a -con_map ) " {x} iff g in Cad ) by A3; :: thesis: verum

end;

hence card ((a -con_map ) " {x}) = card (Centralizer a) by A2, TARSKI:2; :: thesis: verum