let E be non empty finite set ; :: thesis:
let G be finite Group; :: thesis:
let p be Prime; :: thesis:
let T be LeftOperation of G,E; :: thesis:
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 S₁[ 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 S₁[x,y]

let x be object ; :: thesis:
assume A2: x in the_fixed_points_of T ; :: thesis:
then reconsider x9 = x as Element of E ;
reconsider y = the_orbit_of (x9,T) as set ;
take y ; :: thesis:

set X = y;
set x = x9;
take x = x9; :: thesis:
take X = y; :: thesis:
thus ( x9 = x & y = X & X = the_orbit_of (x,T) ) ; :: thesis:
the_fixed_points_of T = { x99 where x99 is Element of E : x99 is_fixed_under T } by Def13;
then ex e being Element of E st
( x = e & e is_fixed_under T ) by A2;
hence x is_fixed_under T ; :: thesis:

end;

hence S₁[x,y] ; :: thesis:

end;

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
S₁[x,FX . x] ) ) from CLASSES1:sch 1(A1);

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

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) ) } ; :: thesis:
then 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; :: thesis:

now :: thesis:

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 ; :: thesis:
set 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; :: thesis:

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; :: thesis:

end;

given x being object such that A12: [x,y] in FX ; :: thesis:
( 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; :: thesis:

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 :: thesis:

let x1, x2 be object ; :: thesis:
assume x1 in dom FX ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
then {x19} = the_orbit_of (x29,T) by A18, A20, Th7
.= {x29} by A21, Th7 ;
hence x1 = x2 by A17, A19, ZFMISC_1:3; :: thesis:

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;

A23: now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in the_orbits_of T ; :: thesis:
then consider X being Subset of E such that
A24: y = X and
A25: ex x being Element of E st X = the_orbit_of (x,T) ;
not X is empty by A25;
then 0 + 1 < (card X) + 1 by XREAL_1:6;
then A26: 1 <= card X by NAT_1:13;

per cases by A26, XXREAL_0:1;

suppose 1 = card X ; :: thesis:

then 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 A24, A25;
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) ) } \/ { 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 3; :: thesis:

end;

suppose 1 < card X ; :: thesis:

then 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 A24, A25;
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) ) } \/ { 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 3; :: thesis:

end;

assume A27: 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 where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; :: thesis:

per cases by A27, XBOOLE_0:def 3;

suppose 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) ) } ; :: thesis:

then ex X being Subset of E st
( y = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ;
hence y in the_orbits_of T ; :: thesis:

end;

suppose 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) ) } ; :: thesis:

then ex X being Subset of E st
( y = X & card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ;
hence y in the_orbits_of T ; :: thesis:

end;

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;

now :: thesis:

given x being object such that A34: x 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 where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; :: thesis:
x 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 A34, XBOOLE_0:def 4;
then A35: ex X being Subset of E st
( x = X & card X > 1 & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ;
x 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 A34, XBOOLE_0:def 4;
then ex X being Subset of E st
( x = X & card X = 1 & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ;
hence contradiction by A35; :: thesis:

end;

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 H₁( 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 = H₁(i) ) ) from FINSEQ_1:sch 2();
for x being object st x in rng p1 holds
x in NAT

proof

let x be object ; :: thesis:
assume x in rng p1 ; :: thesis:
then consider i being Nat such that
A38: i in dom p1 and
A39: p1 . i = x by FINSEQ_2:10;
i in dom f1 by A37, A38, FINSEQ_3:29;
then f1 . 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 A29, FUNCT_1:3;
then A40: ex X being Subset of E st
( f1 . i = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ;
x = card (f1 . i) by A37, A38, A39;
hence x in NAT by A40; :: thesis:

end;

then rng p1 c= NAT ;
then reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def 4;
deffunc H₂( 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 = H₂(i) ) ) from FINSEQ_1:sch 2();
for x being object st x in rng p2 holds
x in NAT

proof

let x be object ; :: thesis:
assume x in rng p2 ; :: thesis:
then consider i being Nat such that
A42: i in dom p2 and
A43: p2 . i = x by FINSEQ_2:10;
i in dom f2 by A41, A42, 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 A44: ex X being Subset of E st
( f2 . i = X & card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ;
x = card (f2 . i) by A41, A42, A43;
hence x in NAT by A44; :: thesis:

end;

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)

proof

let i be Element of NAT ; :: thesis:
assume A46: i in dom c ; :: thesis:

now :: thesis:

per cases by A46, FINSEQ_1:25;

suppose A47: i in dom c1 ; :: thesis:

then A48: i in dom f1 by A37, FINSEQ_3:29;
c . i = c1 . i by A47, FINSEQ_1:def 7
.= card (f1 . i) by A37, A47
.= card (f . i) by A48, FINSEQ_1:def 7 ;
hence c . i = card (f . i) ; :: thesis:

end;

suppose ex j being Nat st
( j in dom c2 & i = (len c1) + j ) ; :: thesis:

then consider j being Nat such that
A49: j in dom c2 and
A50: i = (len c1) + j ;
A51: j in dom f2 by A41, A49, FINSEQ_3:29;
c . i = c2 . j by A49, A50, FINSEQ_1:def 7
.= card (f2 . j) by A41, A49
.= card (f . i) by A37, A50, A51, FINSEQ_1:def 7 ;
hence c . i = card (f . i) ; :: thesis:

end;

hence c . i = card (f . i) ; :: thesis:

end;

assume A52: G is p -group ; :: thesis:
for i being Element of NAT st i in dom c2 holds
p9 divides c2 /. i

proof

let i be Element of NAT ; :: thesis:
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 ; :: thesis:
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;

A62: now :: thesis:

assume card (the_strict_stabilizer_of (x,T)) = card G ; :: thesis:
then card G = (card G) * (index (the_strict_stabilizer_of (x,T))) by GROUP_2:147;
then 1 = ((card G) * (index (the_strict_stabilizer_of (x,T)))) / (card G) by XCMPLX_1:60;
then 1 = ((card G) / (card G)) * (index (the_strict_stabilizer_of (x,T))) by XCMPLX_1:74;
then 1 * (index (the_strict_stabilizer_of (x,T))) = 1 by XCMPLX_1:60;
hence contradiction by A56, A58, A61, GROUP_2:def 18; :: thesis:

end;

per cases by A60, PEPIN:32;

suppose c2 /. i = 1 ; :: thesis:

hence p9 divides c2 /. i by A59, A62; :: thesis:

end;

suppose ex k being Element of NAT st c2 /. i = p * k ; :: thesis:

hence p9 divides c2 /. i by NAT_D:def 3; :: thesis:

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

proof

let i be Element of NAT ; :: thesis:
assume A66: i in dom c1 ; :: thesis:
then i in dom f1 by A37, FINSEQ_3:29;
then f1 . 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 A29, FUNCT_1:3;
then ex X being Subset of E st
( f1 . i = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ;
hence c1 . i = 1 by A37, A66; :: thesis:

end;

for x being object st x in rng c1 holds
x in {1}

proof

let x be object ; :: thesis:
assume x in rng c1 ; :: thesis:
then ex i being Nat st
( i in dom c1 & x = c1 . i ) by FINSEQ_2:10;
then x = 1 by A65;
hence x in {1} by TARSKI:def 1; :: thesis:

end;

then A67: rng c1 c= {1} ;
A68: Sum c1 = len c1

proof

per cases ;

suppose len c1 = 0 ; :: thesis:

then c1 = {} ;
hence Sum c1 = len c1 by RVSUM_1:72; :: thesis:

end;

suppose A69: len c1 <> 0 ; :: thesis:

for x being object st x in {1} holds
x in rng c1

proof

let x be object ; :: thesis:
assume A70: x in {1} ; :: thesis:
A71: Seg (len c1) = dom c1 by FINSEQ_1:def 3;
then c1 . (len c1) = 1 by A65, A69, FINSEQ_1:3;
then c1 . (len c1) = x by A70, TARSKI:def 1;
hence x in rng c1 by A69, A71, FINSEQ_1:3, FUNCT_1:3; :: thesis:

end;

then {1} c= rng c1 ;
then rng c1 = {1} by A67, XBOOLE_0:def 10;
then c1 = (dom c1) --> 1 by FUNCOP_1:9;
then c1 = (Seg (len c1)) --> 1 by FINSEQ_1:def 3;
then c1 = (len c1) |-> 1 by FINSEQ_2:def 2;
then Sum c1 = (len c1) * 1 by RVSUM_1:80;
hence Sum c1 = len c1 ; :: thesis:

end;

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; :: thesis: