let G be Group; for A being Subset of G holds card (con_class A) = Index (Normalizer A)
let A be Subset of G; 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]
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 ;
( x in con_class A & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume
x in con_class A
;
( 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
;
( 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
;
y1 = y2
A =
(A |^ b) |^ (a ")
by A8, A10, Th54
.=
A |^ (b * (a "))
by Th47
;
then
b * (a ") in Normalizer A
by Th129;
hence
y1 = y2
by A9, A11, GROUP_2:120;
verum
end;
A12:
rng f = Right_Cosets (Normalizer A)
f is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( 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
;
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;
b * (a ") in Normalizer A
by A18, A22, A20, GROUP_2:120;
then
ex
h being
Element of
G st
(
b * (a ") = h &
A |^ h = A )
by Th129;
then
A = (A |^ b) |^ (a ")
by Th47;
hence
x = y
by A21, A19, Th54;
verum
end;
then
con_class A, Right_Cosets (Normalizer A) are_equipotent
by A5, A12, WELLORD2:def 4;
hence card (con_class A) =
card (Right_Cosets (Normalizer A))
by CARD_1:5
.=
Index (Normalizer A)
by GROUP_2:145
;
verum