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 syl5bi
 |-  ( 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 syl5bb
 |-  ( 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 syl6bi
 |-  ( 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 ) )