Metamath Proof Explorer

Theorem hashecclwwlkn1

Description: The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 1-May-2021)

Ref Expression
Hypotheses erclwwlkn.w 
|- W = ( N ClWWalksN G )
erclwwlkn.r 
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion hashecclwwlkn1 
|- ( ( N e. Prime /\ U e. ( W /. .~ ) ) -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r 
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 1 2 eclclwwlkn1 
 |-  ( U e. ( W /. .~ ) -> ( U e. ( W /. .~ ) <-> E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
4 rabeq 
 |-  ( W = ( N ClWWalksN G ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
5 1 4 mp1i 
 |-  ( ( N e. Prime /\ x e. W ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
6 prmnn 
 |-  ( N e. Prime -> N e. NN )
7 6 nnnn0d 
 |-  ( N e. Prime -> N e. NN0 )
8 1 eleq2i 
 |-  ( x e. W <-> x e. ( N ClWWalksN G ) )
9 8 biimpi 
 |-  ( x e. W -> x e. ( N ClWWalksN G ) )
10 clwwlknscsh 
 |-  ( ( N e. NN0 /\ x e. ( N ClWWalksN G ) ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
11 7 9 10 syl2an 
 |-  ( ( N e. Prime /\ x e. W ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
12 5 11 eqtrd 
 |-  ( ( N e. Prime /\ x e. W ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
13 12 eqeq2d 
 |-  ( ( N e. Prime /\ x e. W ) -> ( U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
14 simpll 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> x e. Word ( Vtx ` G ) )
15 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
16 eqeq1 
 |-  ( N = ( # ` x ) -> ( N = 0 <-> ( # ` x ) = 0 ) )
17 16 eqcoms 
 |-  ( ( # ` x ) = N -> ( N = 0 <-> ( # ` x ) = 0 ) )
18 hasheq0 
 |-  ( x e. Word ( Vtx ` G ) -> ( ( # ` x ) = 0 <-> x = (/) ) )
19 17 18 sylan9bbr 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N = 0 <-> x = (/) ) )
20 19 necon3bid 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N =/= 0 <-> x =/= (/) ) )
21 20 biimpcd 
 |-  ( N =/= 0 -> ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> x =/= (/) ) )
22 15 21 simplbiim 
 |-  ( N e. NN -> ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> x =/= (/) ) )
23 22 impcom 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> x =/= (/) )
24 simplr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> ( # ` x ) = N )
25 24 eqcomd 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> N = ( # ` x ) )
26 14 23 25 3jca 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) )
27 26 ex 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N e. NN -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 28 clwwlknbp 
 |-  ( x e. ( N ClWWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) )
30 27 29 syl11 
 |-  ( N e. NN -> ( x e. ( N ClWWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
31 8 30 biimtrid 
 |-  ( N e. NN -> ( x e. W -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
32 6 31 syl 
 |-  ( N e. Prime -> ( x e. W -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
33 32 imp 
 |-  ( ( N e. Prime /\ x e. W ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) )
34 scshwfzeqfzo 
 |-  ( ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } )
35 33 34 syl 
 |-  ( ( N e. Prime /\ x e. W ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } )
36 35 eqeq2d 
 |-  ( ( N e. Prime /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } ) )
37 oveq2 
 |-  ( n = m -> ( x cyclShift n ) = ( x cyclShift m ) )
38 37 eqeq2d 
 |-  ( n = m -> ( y = ( x cyclShift n ) <-> y = ( x cyclShift m ) ) )
39 38 cbvrexvw 
 |-  ( E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) <-> E. m e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift m ) )
40 eqeq1 
 |-  ( y = u -> ( y = ( x cyclShift m ) <-> u = ( x cyclShift m ) ) )
41 eqcom 
 |-  ( u = ( x cyclShift m ) <-> ( x cyclShift m ) = u )
42 40 41 bitrdi 
 |-  ( y = u -> ( y = ( x cyclShift m ) <-> ( x cyclShift m ) = u ) )
43 42 rexbidv 
 |-  ( y = u -> ( E. m e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift m ) <-> E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u ) )
44 39 43 bitrid 
 |-  ( y = u -> ( E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) <-> E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u ) )
45 44 cbvrabv 
 |-  { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } = { u e. Word ( Vtx ` G ) | E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u }
46 45 cshwshash 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) -> ( ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) \/ ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 ) )
47 46 adantr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) /\ U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) -> ( ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) \/ ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 ) )
48 47 orcomd 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) /\ U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) -> ( ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 \/ ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) )
49 fveqeq2 
 |-  ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 <-> ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 ) )
50 fveqeq2 
 |-  ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = ( # ` x ) <-> ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) )
51 49 50 orbi12d 
 |-  ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) <-> ( ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 \/ ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) ) )
52 51 adantl 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) /\ U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) -> ( ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) <-> ( ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = 1 \/ ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) ) )
53 48 52 mpbird 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) /\ U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) )
54 53 ex 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) )
55 54 ex 
 |-  ( x e. Word ( Vtx ` G ) -> ( ( # ` x ) e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) )
56 55 adantr 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( ( # ` x ) e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) )
57 eleq1 
 |-  ( N = ( # ` x ) -> ( N e. Prime <-> ( # ` x ) e. Prime ) )
58 oveq2 
 |-  ( N = ( # ` x ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` x ) ) )
59 58 rexeqdv 
 |-  ( N = ( # ` x ) -> ( E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) <-> E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) ) )
60 59 rabbidv 
 |-  ( N = ( # ` x ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } )
61 60 eqeq2d 
 |-  ( N = ( # ` x ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) )
62 eqeq2 
 |-  ( N = ( # ` x ) -> ( ( # ` U ) = N <-> ( # ` U ) = ( # ` x ) ) )
63 62 orbi2d 
 |-  ( N = ( # ` x ) -> ( ( ( # ` U ) = 1 \/ ( # ` U ) = N ) <-> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) )
64 61 63 imbi12d 
 |-  ( N = ( # ` x ) -> ( ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) <-> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) )
65 57 64 imbi12d 
 |-  ( N = ( # ` x ) -> ( ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) <-> ( ( # ` x ) e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) ) )
66 65 eqcoms 
 |-  ( ( # ` x ) = N -> ( ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) <-> ( ( # ` x ) e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) ) )
67 66 adantl 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) <-> ( ( # ` x ) e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = ( # ` x ) ) ) ) ) )
68 56 67 mpbird 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) )
69 29 68 syl 
 |-  ( x e. ( N ClWWalksN G ) -> ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) )
70 69 1 eleq2s 
 |-  ( x e. W -> ( N e. Prime -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) )
71 70 impcom 
 |-  ( ( N e. Prime /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
72 36 71 sylbid 
 |-  ( ( N e. Prime /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
73 13 72 sylbid 
 |-  ( ( N e. Prime /\ x e. W ) -> ( U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
74 73 rexlimdva 
 |-  ( N e. Prime -> ( E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
75 74 com12 
 |-  ( E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( N e. Prime -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
76 3 75 biimtrdi 
 |-  ( U e. ( W /. .~ ) -> ( U e. ( W /. .~ ) -> ( N e. Prime -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) ) )
77 76 pm2.43i 
 |-  ( U e. ( W /. .~ ) -> ( N e. Prime -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) ) )
78 77 impcom 
 |-  ( ( N e. Prime /\ U e. ( W /. .~ ) ) -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) )