let E be non empty finite set ; for G being finite Group
for p being prime Nat
for T being LeftOperation of G,E st G is p -group holds
(card (the_fixed_points_of T)) mod p = (card E) mod p
let G be finite Group; for p being prime Nat
for T being LeftOperation of G,E st G is p -group holds
(card (the_fixed_points_of T)) mod p = (card E) mod p
let p be prime Nat; for T being LeftOperation of G,E st G is p -group holds
(card (the_fixed_points_of T)) mod p = (card E) mod p
let T be LeftOperation of G,E; ( G is p -group implies (card (the_fixed_points_of T)) mod p = (card E) mod p )
set O1 = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ;
set O2 = { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ;
set O = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ;
defpred S1[ object , object ] means ex x being Element of E ex X being Subset of E st
( $1 = x & $2 = X & X = the_orbit_of (x,T) & x is_fixed_under T );
reconsider p9 = p as Element of NAT by ORDINAL1:def 12;
A1:
for x being object st x in the_fixed_points_of T holds
ex y being object st S1[x,y]
consider FX being Function such that
A3:
( dom FX = the_fixed_points_of T & ( for x being object st x in the_fixed_points_of T holds
S1[x,FX . x] ) )
from CLASSES1:sch 1(A1);
now for y being object holds
( ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } implies ex x being object st [x,y] in FX ) & ( ex x being object st [x,y] in FX implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) )let y be
object ;
( ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } implies ex x being object st [x,y] in FX ) & ( ex x being object st [x,y] in FX implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) )hereby ( ex x being object st [x,y] in FX implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } )
assume
y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
;
ex x being object st [x,y] in FXthen consider X being
Subset of
E such that A4:
y = X
and A5:
card X = 1
and A6:
ex
x being
Element of
E st
X = the_orbit_of (
x,
T)
;
consider x9 being
Element of
E such that A7:
X = the_orbit_of (
x9,
T)
by A6;
reconsider x =
x9 as
object ;
card X = card {x}
by A5, CARD_1:30;
then consider x99 being
object such that A8:
X = {x99}
by CARD_1:29;
take x =
x;
[x,y] in FXnow for g being Element of G holds not x9 <> (T ^ g) . x9
x9,
x9 are_conjugated_under T
by Th3;
then A9:
x9 in { y99 where y99 is Element of E : x9,y99 are_conjugated_under T }
;
given g being
Element of
G such that A10:
x9 <> (T ^ g) . x9
;
contradictionset y9 =
(T ^ g) . x9;
x9,
(T ^ g) . x9 are_conjugated_under T
;
then
(T ^ g) . x9 in { y99 where y99 is Element of E : x9,y99 are_conjugated_under T }
;
then
(T ^ g) . x9 = x99
by A7, A8, TARSKI:def 1;
hence
contradiction
by A7, A8, A10, A9, TARSKI:def 1;
verum end; then
x9 is_fixed_under T
;
then
x in { x999 where x999 is Element of E : x999 is_fixed_under T }
;
then A11:
x in the_fixed_points_of T
by Def13;
then
ex
x99 being
Element of
E ex
X9 being
Subset of
E st
(
x99 = x &
X9 = FX . x &
X9 = the_orbit_of (
x99,
T) &
x99 is_fixed_under T )
by A3;
hence
[x,y] in FX
by A3, A4, A7, A11, FUNCT_1:1;
verum
end; given x being
object such that A12:
[x,y] in FX
;
y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
(
x in dom FX &
y = FX . x )
by A12, FUNCT_1:1;
then consider x9 being
Element of
E,
X9 being
Subset of
E such that
x9 = x
and A13:
X9 = y
and A14:
X9 = the_orbit_of (
x9,
T)
and A15:
x9 is_fixed_under T
by A3;
X9 = {x9}
by A14, A15, Th7;
then
card X9 = 1
by CARD_1:30;
hence
y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
by A13, A14;
verum end;
then A16:
rng FX = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
by XTUPLE_0:def 13;
now for x1, x2 being object st x1 in dom FX & x2 in dom FX & FX . x1 = FX . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom FX & x2 in dom FX & FX . x1 = FX . x2 implies x1 = x2 )assume
x1 in dom FX
;
( x2 in dom FX & FX . x1 = FX . x2 implies x1 = x2 )then consider x19 being
Element of
E,
X1 being
Subset of
E such that A17:
x19 = x1
and A18:
(
X1 = FX . x1 &
X1 = the_orbit_of (
x19,
T) &
x19 is_fixed_under T )
by A3;
assume
x2 in dom FX
;
( FX . x1 = FX . x2 implies x1 = x2 )then consider x29 being
Element of
E,
X2 being
Subset of
E such that A19:
x29 = x2
and A20:
(
X2 = FX . x2 &
X2 = the_orbit_of (
x29,
T) )
and A21:
x29 is_fixed_under T
by A3;
assume
FX . x1 = FX . x2
;
x1 = x2then {x19} =
the_orbit_of (
x29,
T)
by A18, A20, Th7
.=
{x29}
by A21, Th7
;
hence
x1 = x2
by A17, A19, ZFMISC_1:3;
verum end;
then
FX is one-to-one
by FUNCT_1:def 4;
then A22:
the_fixed_points_of T, { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } are_equipotent
by A3, A16;
then A28:
{ X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } = the_orbits_of T
by TARSKI:2;
then
{ X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } is finite
by FINSET_1:1, XBOOLE_1:7;
then consider f1 being FinSequence such that
A29:
rng f1 = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
and
A30:
f1 is one-to-one
by FINSEQ_4:58;
{ X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } is finite
by A28, FINSET_1:1, XBOOLE_1:7;
then consider f2 being FinSequence such that
A31:
rng f2 = { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
and
A32:
f2 is one-to-one
by FINSEQ_4:58;
set f = f1 ^ f2;
reconsider O = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } as a_partition of E by A23, TARSKI:2;
A33:
rng (f1 ^ f2) = O
by A29, A31, FINSEQ_1:31;
then
{ X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } /\ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } = {}
by XBOOLE_0:def 1;
then
rng f1 misses rng f2
by A29, A31, XBOOLE_0:def 7;
then A36:
f1 ^ f2 is one-to-one
by A30, A32, FINSEQ_3:91;
reconsider f = f1 ^ f2 as FinSequence of O by A33, FINSEQ_1:def 4;
deffunc H1( set ) -> set = card (f1 . $1);
consider p1 being FinSequence such that
A37:
( len p1 = len f1 & ( for i being Nat st i in dom p1 holds
p1 . i = H1(i) ) )
from FINSEQ_1:sch 2();
for x being object st x in rng p1 holds
x in NAT
then
rng p1 c= NAT
;
then reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def 4;
deffunc H2( set ) -> set = card (f2 . $1);
consider p2 being FinSequence such that
A41:
( len p2 = len f2 & ( for i being Nat st i in dom p2 holds
p2 . i = H2(i) ) )
from FINSEQ_1:sch 2();
for x being object st x in rng p2 holds
x in NAT
then
rng p2 c= NAT
;
then reconsider c2 = p2 as FinSequence of NAT by FINSEQ_1:def 4;
set c = c1 ^ c2;
reconsider c = c1 ^ c2 as FinSequence of NAT ;
A45:
for i being Element of NAT st i in dom c holds
c . i = card (f . i)
assume A52:
G is p -group
; (card (the_fixed_points_of T)) mod p = (card E) mod p
for i being Element of NAT st i in dom c2 holds
p9 divides c2 /. i
proof
let i be
Element of
NAT ;
( i in dom c2 implies p9 divides c2 /. i )
set i9 =
c2 /. i;
consider r being
Nat such that A53:
card G = p |^ r
by A52;
reconsider r9 =
r as
Element of
NAT by ORDINAL1:def 12;
assume A54:
i in dom c2
;
p9 divides c2 /. i
then
i in dom f2
by A41, FINSEQ_3:29;
then
f2 . i in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) }
by A31, FUNCT_1:3;
then consider X being
Subset of
E such that A55:
f2 . i = X
and A56:
card X > 1
and A57:
ex
x being
Element of
E st
X = the_orbit_of (
x,
T)
;
consider x being
Element of
E such that A58:
X = the_orbit_of (
x,
T)
by A57;
set H =
the_strict_stabilizer_of (
x,
T);
c2 . i = card (f2 . i)
by A41, A54;
then
c2 /. i = card (f2 . i)
by A54, PARTFUN1:def 6;
then
c2 /. i = Index (the_strict_stabilizer_of (x,T))
by A55, A58, Th8;
then
c2 /. i = index (the_strict_stabilizer_of (x,T))
by GROUP_2:def 18;
then A59:
card G = (card (the_strict_stabilizer_of (x,T))) * (c2 /. i)
by GROUP_2:147;
then A60:
c2 /. i divides p9 |^ r9
by A53, NAT_D:def 3;
A61:
card (the_orbit_of (x,T)) = Index (the_strict_stabilizer_of (x,T))
by Th8;
end;
then
p divides Sum c2
by WEDDWITT:5;
then
ex t being Nat st Sum c2 = p * t
by NAT_D:def 3;
then A63:
(Sum c2) mod p = 0
by NAT_D:13;
len c = (len f1) + (len f2)
by A37, A41, FINSEQ_1:22;
then
len c = len f
by FINSEQ_1:22;
then card E =
Sum c
by A36, A33, A45, WEDDWITT:6
.=
(Sum c1) + (Sum c2)
by RVSUM_1:75
;
then A64: (card E) mod p =
((Sum c1) + ((Sum c2) mod p)) mod p
by NAT_D:23
.=
(Sum c1) mod p
by A63
;
A65:
for i being Element of NAT st i in dom c1 holds
c1 . i = 1
for x being object st x in rng c1 holds
x in {1}
then A67:
rng c1 c= {1}
;
A68:
Sum c1 = len c1
len c1 = card (rng f1)
by A30, A37, FINSEQ_4:62;
hence
(card (the_fixed_points_of T)) mod p = (card E) mod p
by A29, A68, A22, A64, CARD_1:5; verum