let G be addGroup; :: thesis: for A being Subset of G holds card (con_class A) = Index (Normalizer A)
let A be Subset of G; :: thesis: card (con_class A) = Index (Normalizer A)
defpred S1[ object , object ] means ex a being Element of G st
( $1 = A * a & $2 = (Normalizer A) + a );
A1: for x being object st x in con_class A holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in con_class A implies ex y being object st S1[x,y] )
assume x in con_class A ; :: thesis: ex y being object st S1[x,y]
then consider B being Subset of G such that
A2: x = B and
A3: A,B are_conjugated ;
consider g being Element of G such that
A4: B = A * g by A3, Th88;
reconsider y = (Normalizer A) + g as set ;
take y ; :: thesis: S1[x,y]
take g ; :: thesis: ( x = A * g & y = (Normalizer A) + g )
thus ( x = A * g & y = (Normalizer A) + g ) by A2, A4; :: thesis: verum
end;
consider f being Function such that
A5: dom f = con_class A and
A6: for x being object st x in con_class A holds
S1[x,f . x] from CLASSES1:sch 1(A1);
 A7: for x, y1, y2 being set st x in con_class A & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be set ; :: thesis: ( x in con_class A & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume x in con_class A ; :: thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 )
given a being Element of G such that A8: x = A * a and
A9: y1 = (Normalizer A) + a ; :: thesis: ( not S1[x,y2] or y1 = y2 )
given b being Element of G such that A10: x = A * b and
A11: y2 = (Normalizer A) + b ; :: thesis: y1 = y2
A = (A * b) * (- a) by A8, A10, Th54
.= A * (b + (- a)) by Th47 ;
hence y1 = y2 by A9, A11, Th129, Th120; :: thesis: verum
end;
A12: rng f = Right_Cosets (Normalizer A)
proof
thus rng f c= Right_Cosets (Normalizer A) :: according to XBOOLE_0:def 10 :: thesis: Right_Cosets (Normalizer A) c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Right_Cosets (Normalizer A) )
assume x in rng f ; :: thesis: x in Right_Cosets (Normalizer A)
then consider y being object such that
A13: ( y in dom f & f . y = x ) by FUNCT_1:def 3;
ex a being Element of G st
( y = A * a & x = (Normalizer A) + a ) by A5, A6, A13;
hence x in Right_Cosets (Normalizer A) by Def16; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Right_Cosets (Normalizer A) or x in rng f )
assume x in Right_Cosets (Normalizer A) ; :: thesis: x in rng f
then consider a being Element of G such that
A14: x = (Normalizer A) + a by Def16;
set y = A * a;
A,A * a are_conjugated by Th88;
then A15: A * a in con_class A ;
then ex b being Element of G st
( A * a = A * b & f . (A * a) = (Normalizer A) + b ) by A6;
then x = f . (A * a) by A7, A14, A15;
hence x in rng f by A5, A15, FUNCT_1:def 3; :: thesis: verum
end;
f is one-to-one
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A16: x in dom f and
A17: y in dom f and
A18: f . x = f . y ; :: thesis: x = y
consider b being Element of G such that
A19: y = A * b and
A20: f . y = (Normalizer A) + b by A5, A6, A17;
consider a being Element of G such that
A21: x = A * a and
A22: f . x = (Normalizer A) + a by A5, A6, A16;
ex h being Element of G st
( b + (- a) = h & A * h = A ) by A18, A20, A22, Th129, Th120;
then A = (A * b) * (- a) by Th47;
hence x = y by A21, A19, Th54; :: thesis: verum
end;
hence card (con_class A) = card (Right_Cosets (Normalizer A)) by A5, A12, WELLORD2:def 4, CARD_1:5
.= Index (Normalizer A) by Th145 ;
:: thesis: verum