let G be finite Group; :: thesis: for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))

let a be Element of G; :: thesis: card G = (card (con_class a)) * (card (Centralizer a))

reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as a_partition of the carrier of G by Th11;

A1: for A being set st A in X holds

( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) )

for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

A8: C = union X and

A9: card C = (card X) * k by GROUP_2:156;

card G = card C by A8, EQREL_1:def 4

.= (card (con_class a)) * (card (Centralizer a)) by A9, Th12 ;

hence card G = (card (con_class a)) * (card (Centralizer a)) ; :: thesis: verum

let a be Element of G; :: thesis: card G = (card (con_class a)) * (card (Centralizer a))

reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as a_partition of the carrier of G by Th11;

A1: for A being set st A in X holds

( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) )

proof

reconsider k = card (Centralizer a) as Element of NAT ;
let A be set ; :: thesis: ( A in X implies ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) ) )

assume A2: A in X ; :: thesis: ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) )

reconsider A = A as Subset of G by A2;

ex x being Element of con_class a st A = (a -con_map) " {x} by A2;

hence ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) ) by A2, Th9, EQREL_1:def 4; :: thesis: verum

end;A misses B ) ) )

assume A2: A in X ; :: thesis: ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) )

reconsider A = A as Subset of G by A2;

ex x being Element of con_class a st A = (a -con_map) " {x} by A2;

hence ( A is finite & card A = card (Centralizer a) & ( for B being set st B in X & A <> B holds

A misses B ) ) by A2, Th9, EQREL_1:def 4; :: thesis: verum

for Y being set st Y in X holds

ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

proof

then consider C being finite set such that
let Y be set ; :: thesis: ( Y in X implies ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) )

assume A3: Y in X ; :: thesis: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

reconsider Y = Y as finite set by A3;

A4: card Y = card (Centralizer a) by A1, A3;

for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z )

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A4; :: thesis: verum

end;( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) )

assume A3: Y in X ; :: thesis: ex B being finite set st

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) )

reconsider Y = Y as finite set by A3;

A4: card Y = card (Centralizer a) by A1, A3;

for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z )

proof

hence
ex B being finite set st
let Z be set ; :: thesis: ( Z in X & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )

assume that

A5: Z in X and

A6: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )

A7: card Y = card (Centralizer a) by A1, A3;

card Z = card (Centralizer a) by A1, A5;

hence ( Y,Z are_equipotent & Y misses Z ) by A1, A3, A5, A6, A7, CARD_1:5; :: thesis: verum

end;assume that

A5: Z in X and

A6: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )

A7: card Y = card (Centralizer a) by A1, A3;

card Z = card (Centralizer a) by A1, A5;

hence ( Y,Z are_equipotent & Y misses Z ) by A1, A3, A5, A6, A7, CARD_1:5; :: thesis: verum

( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds

( Y,Z are_equipotent & Y misses Z ) ) ) by A4; :: thesis: verum

A8: C = union X and

A9: card C = (card X) * k by GROUP_2:156;

card G = card C by A8, EQREL_1:def 4

.= (card (con_class a)) * (card (Centralizer a)) by A9, Th12 ;

hence card G = (card (con_class a)) * (card (Centralizer a)) ; :: thesis: verum