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:80;

then consider d being Element of G such that

A1: x = a |^ d by GROUP_3:74;

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:133;

for g being object holds

( g in (a -con_map) " {x} iff g in Cad )

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:80;

then consider d being Element of G such that

A1: x = a |^ d by GROUP_3:74;

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:133;

for g being object holds

( g in (a -con_map) " {x} iff g in Cad )

proof

hence
card ((a -con_map) " {x}) = card (Centralizer a)
by A2, TARSKI:2; :: thesis: verum
let g be object ; :: thesis: ( g in (a -con_map) " {x} iff g in Cad )

end;A3: now :: thesis: ( g in (a -con_map) " {x} implies g in Cad )

assume A4:
g in (a -con_map) " {x}
; :: thesis: g in Cad

then (a -con_map) . g in {x} by FUNCT_1:def 7;

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 3

.= ((y * (d ")) * a) * d by GROUP_1:def 3 ;

y * (((y ") * a) * y) = (y * ((y ") * a)) * y by GROUP_1:def 3

.= a * y by GROUP_3:1 ;

then (((y * (d ")) * a) * d) * (d ") = a * (y * (d ")) by A1, A5, A6, A7, GROUP_1:def 3;

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;

reconsider z = z as Element of G ;

y = z * d by A9, GROUP_3:1;

hence g in Cad by A10, GROUP_2:104; :: thesis: verum

end;then (a -con_map) . g in {x} by FUNCT_1:def 7;

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 3

.= ((y * (d ")) * a) * d by GROUP_1:def 3 ;

y * (((y ") * a) * y) = (y * ((y ") * a)) * y by GROUP_1:def 3

.= a * y by GROUP_3:1 ;

then (((y * (d ")) * a) * d) * (d ") = a * (y * (d ")) by A1, A5, A6, A7, GROUP_1:def 3;

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;

reconsider z = z as Element of G ;

y = z * d by A9, GROUP_3:1;

hence g in Cad by A10, GROUP_2:104; :: thesis: verum

now :: thesis: ( g in Cad implies g in (a -con_map) " {x} )

hence
( g in (a -con_map) " {x} iff g in Cad )
by A3; :: thesis: verumassume
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:104;

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;

then (y * (d ")) * a = a * (y * (d ")) by Th8;

then ((y * (d ")) * a) * d = a * ((y * (d ")) * d) by GROUP_1:def 3;

then ((y * (d ")) * a) * d = a * y by GROUP_3:1;

then (y * (d ")) * (a * d) = a * y by GROUP_1:def 3;

then (y ") * ((y * (d ")) * (a * d)) = ((y ") * a) * y by GROUP_1:def 3;

then ((y ") * (y * (d "))) * (a * d) = ((y ") * a) * y by GROUP_1:def 3;

then (d ") * (a * d) = ((y ") * a) * y by GROUP_3:1;

then x = a |^ y by A1, GROUP_1:def 3;

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 7; :: thesis: verum

end;then consider z being Element of G such that

A11: g = z * d and

A12: z in Centralizer a by GROUP_2:104;

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;

then (y * (d ")) * a = a * (y * (d ")) by Th8;

then ((y * (d ")) * a) * d = a * ((y * (d ")) * d) by GROUP_1:def 3;

then ((y * (d ")) * a) * d = a * y by GROUP_3:1;

then (y * (d ")) * (a * d) = a * y by GROUP_1:def 3;

then (y ") * ((y * (d ")) * (a * d)) = ((y ") * a) * y by GROUP_1:def 3;

then ((y ") * (y * (d "))) * (a * d) = ((y ") * a) * y by GROUP_1:def 3;

then (d ") * (a * d) = ((y ") * a) * y by GROUP_3:1;

then x = a |^ y by A1, GROUP_1:def 3;

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 7; :: thesis: verum