let G be Group; :: thesis: for E being non empty set
for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)
let E be non empty set ; :: thesis: for a being Element of E
for T being LeftOperation of G,E holds card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)
let a be Element of E; :: thesis: for T being LeftOperation of G,E holds card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)
let T be LeftOperation of G,E; :: thesis: card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)
set H = the_strict_stabilizer_of a,T;
set f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } ;
reconsider A' = {a} as Subset of E ;
A1:
now let x be
set ;
:: thesis: ( x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } implies ex b, A being set st x = [b,A] )assume
x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) }
;
:: thesis: ex b, A being set st x = [b,A]then consider b being
Element of
E,
A being
Subset of
G such that A2:
(
[b,A] = x & ex
g being
Element of
G st
(
b = (T ^ g) . a &
A = g * (the_strict_stabilizer_of a,T) ) )
;
reconsider b =
b,
A =
A as
set ;
take b =
b;
:: thesis: ex A being set st x = [b,A]take A =
A;
:: thesis: x = [b,A]thus
x = [b,A]
by A2;
:: thesis: verum end;
now let x,
y1,
y2 be
set ;
:: thesis: ( [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } & [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } implies y1 = y2 )assume
[x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) }
;
:: thesis: ( [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } implies y1 = y2 )then consider b1 being
Element of
E,
A1 being
Subset of
G such that A3:
(
[b1,A1] = [x,y1] & ex
g being
Element of
G st
(
b1 = (T ^ g) . a &
A1 = g * (the_strict_stabilizer_of a,T) ) )
;
assume
[x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) }
;
:: thesis: y1 = y2then consider b2 being
Element of
E,
A2 being
Subset of
G such that A4:
(
[b2,A2] = [x,y2] & ex
g being
Element of
G st
(
b2 = (T ^ g) . a &
A2 = g * (the_strict_stabilizer_of a,T) ) )
;
A5:
(
x = b1 &
y1 = A1 )
by A3, ZFMISC_1:33;
A6:
(
x = b2 &
y2 = A2 )
by A4, ZFMISC_1:33;
consider g1 being
Element of
G such that A7:
(
b1 = (T ^ g1) . a &
A1 = g1 * (the_strict_stabilizer_of a,T) )
by A3;
consider g2 being
Element of
G such that A8:
(
b2 = (T ^ g2) . a &
A2 = g2 * (the_strict_stabilizer_of a,T) )
by A4;
A9:
(
dom (T ^ g1) = E &
dom (T ^ g2) = E )
by FUNCT_2:def 1;
(T ^ g1) . a = (T ^ g2) . a
by A3, A6, A7, A8, ZFMISC_1:33;
then
Im (T ^ g1),
a = {((T ^ g2) . a)}
by A9, FUNCT_1:117;
then A10:
Im (T ^ g1),
a = Im (T ^ g2),
a
by A9, FUNCT_1:117;
set g =
(g2 " ) * g1;
reconsider g =
(g2 " ) * g1 as
Element of
G ;
A11:
the
carrier of
(the_strict_stabilizer_of A',T) = { g' where g' is Element of G : (T ^ g') .: A' = A' }
by Def10;
(T ^ g) .: A' =
((T ^ (g2 " )) * (T ^ g1)) .: A'
by Def1
.=
(T ^ (g2 " )) .: ((T ^ g1) .: A')
by RELAT_1:159
.=
((T ^ (g2 " )) * (T ^ g2)) .: A'
by A10, RELAT_1:159
.=
(T ^ ((g2 " ) * g2)) .: A'
by Def1
.=
(T ^ (1_ G)) .: A'
by GROUP_1:def 6
.=
(id E) .: A'
by Def1
.=
A'
by FUNCT_1:162
;
then
g in { g' where g' is Element of G : (T ^ g') .: A' = A' }
;
then
g in the_strict_stabilizer_of A',
T
by A11, STRUCT_0:def 5;
hence
y1 = y2
by A5, A6, A7, A8, GROUP_2:137;
:: thesis: verum end;
then reconsider f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st
( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of a,T) ) } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume
x1 in dom f
;
:: thesis: ( x2 in dom f & f . x1 = f . x2 implies x1 = x2 )then
[x1,(f . x1)] in f
by FUNCT_1:8;
then consider b1 being
Element of
E,
A1 being
Subset of
G such that A12:
(
[b1,A1] = [x1,(f . x1)] & ex
g being
Element of
G st
(
b1 = (T ^ g) . a &
A1 = g * (the_strict_stabilizer_of a,T) ) )
;
assume
x2 in dom f
;
:: thesis: ( f . x1 = f . x2 implies x1 = x2 )then
[x2,(f . x2)] in f
by FUNCT_1:8;
then consider b2 being
Element of
E,
A2 being
Subset of
G such that A13:
(
[b2,A2] = [x2,(f . x2)] & ex
g being
Element of
G st
(
b2 = (T ^ g) . a &
A2 = g * (the_strict_stabilizer_of a,T) ) )
;
A14:
(
x1 = b1 &
f . x1 = A1 )
by A12, ZFMISC_1:33;
A15:
(
x2 = b2 &
f . x2 = A2 )
by A13, ZFMISC_1:33;
consider g1 being
Element of
G such that A16:
(
b1 = (T ^ g1) . a &
A1 = g1 * (the_strict_stabilizer_of a,T) )
by A12;
consider g2 being
Element of
G such that A17:
(
b2 = (T ^ g2) . a &
A2 = g2 * (the_strict_stabilizer_of a,T) )
by A13;
A18:
the
carrier of
(the_strict_stabilizer_of A',T) = { g' where g' is Element of G : (T ^ g') .: A' = A' }
by Def10;
set g =
(g2 " ) * g1;
assume
f . x1 = f . x2
;
:: thesis: x1 = x2then
g1 * (the_strict_stabilizer_of a,T) = g2 * (the_strict_stabilizer_of a,T)
by A12, A15, A16, A17, ZFMISC_1:33;
then
(g2 " ) * g1 in the_strict_stabilizer_of a,
T
by GROUP_2:137;
then
(g2 " ) * g1 in the
carrier of
(the_strict_stabilizer_of A',T)
by STRUCT_0:def 5;
then A19:
ex
g' being
Element of
G st
(
(g2 " ) * g1 = g' &
(T ^ g') .: A' = A' )
by A18;
A20:
(
dom (T ^ g1) = E &
dom (T ^ g2) = E )
by FUNCT_2:def 1;
(T ^ g1) .: A' =
(id E) .: ((T ^ g1) .: A')
by FUNCT_1:162
.=
(T ^ (1_ G)) .: ((T ^ g1) .: A')
by Def1
.=
(T ^ (g2 * (g2 " ))) .: ((T ^ g1) .: A')
by GROUP_1:def 6
.=
((T ^ (g2 * (g2 " ))) * (T ^ g1)) .: A'
by RELAT_1:159
.=
(T ^ ((g2 * (g2 " )) * g1)) .: A'
by Def1
.=
(T ^ (g2 * ((g2 " ) * g1))) .: A'
by GROUP_1:def 4
.=
((T ^ g2) * (T ^ ((g2 " ) * g1))) .: A'
by Def1
.=
(T ^ g2) .: A'
by A19, RELAT_1:159
;
then
Im (T ^ g1),
a = Im (T ^ g2),
a
;
then
Im (T ^ g1),
a = {((T ^ g2) . a)}
by A20, FUNCT_1:117;
then
{((T ^ g1) . a)} = {((T ^ g2) . a)}
by A20, FUNCT_1:117;
hence
x1 = x2
by A14, A15, A16, A17, ZFMISC_1:24;
:: thesis: verum end;
then A21:
f is one-to-one
by FUNCT_1:def 8;
for x being set holds
( x in the_orbit_of a,T iff ex y being set st [x,y] in f )
proof
let x be
set ;
:: thesis: ( x in the_orbit_of a,T iff ex y being set st [x,y] in f )
given y being
set such that A24:
[x,y] in f
;
:: thesis: x in the_orbit_of a,T
consider b being
Element of
E,
A being
Subset of
G such that A25:
(
[b,A] = [x,y] & ex
g being
Element of
G st
(
b = (T ^ g) . a &
A = g * (the_strict_stabilizer_of a,T) ) )
by A24;
A26:
(
b = x &
A = y )
by A25, ZFMISC_1:33;
a,
b are_conjugated_under T
by A25, Def14;
hence
x in the_orbit_of a,
T
by A26;
:: thesis: verum
end;
then A27:
dom f = the_orbit_of a,T
by RELAT_1:def 4;
for y being set holds
( y in Left_Cosets (the_strict_stabilizer_of a,T) iff ex x being set st [x,y] in f )
proof
let y be
set ;
:: thesis: ( y in Left_Cosets (the_strict_stabilizer_of a,T) iff ex x being set st [x,y] in f )
given x being
set such that A30:
[x,y] in f
;
:: thesis: y in Left_Cosets (the_strict_stabilizer_of a,T)
consider b being
Element of
E,
A being
Subset of
G such that A31:
(
[b,A] = [x,y] & ex
g being
Element of
G st
(
b = (T ^ g) . a &
A = g * (the_strict_stabilizer_of a,T) ) )
by A30;
(
b = x &
A = y )
by A31, ZFMISC_1:33;
hence
y in Left_Cosets (the_strict_stabilizer_of a,T)
by A31, GROUP_2:def 15;
:: thesis: verum
end;
then
rng f = Left_Cosets (the_strict_stabilizer_of a,T)
by RELAT_1:def 5;
then
the_orbit_of a,T, Left_Cosets (the_strict_stabilizer_of a,T) are_equipotent
by A21, A27, WELLORD2:def 4;
hence
card (the_orbit_of a,T) = Index (the_strict_stabilizer_of a,T)
by CARD_1:21; :: thesis: verum