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 ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion hashecclwwlkn1 ( ( 𝑁 ∈ ℙ ∧ 𝑈 ∈ ( 𝑊 / ∼ ) ) → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 1 2 eclclwwlkn1 ⊢ ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( 𝑈 ∈ ( 𝑊 / ∼ ) ↔ ∃ 𝑥 ∈ 𝑊 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
4 rabeq ⊢ ( 𝑊 = ( 𝑁 ClWWalksN 𝐺 ) → { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
5 1 4 mp1i ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
6 prmnn ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
7 6 nnnn0d ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ0 )
8 1 eleq2i ⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
9 8 biimpi ⊢ ( 𝑥 ∈ 𝑊 → 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
10 clwwlknscsh ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
11 7 9 10 syl2an ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
12 5 11 eqtrd ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
13 12 eqeq2d ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
14 simpll ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
15 elnnne0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
16 eqeq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑁 = 0 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
17 16 eqcoms ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( 𝑁 = 0 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
18 hasheq0 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
19 17 18 sylan9bbr ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 = 0 ↔ 𝑥 = ∅ ) )
20 19 necon3bid ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 ≠ 0 ↔ 𝑥 ≠ ∅ ) )
21 20 biimpcd ⊢ ( 𝑁 ≠ 0 → ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑥 ≠ ∅ ) )
22 15 21 simplbiim ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑥 ≠ ∅ ) )
23 22 impcom ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑥 ≠ ∅ )
24 simplr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑥 ) = 𝑁 )
25 24 eqcomd ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 = ( ♯ ‘ 𝑥 ) )
26 14 23 25 3jca ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) )
27 26 ex ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 ∈ ℕ → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
28 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29 28 clwwlknbp ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
30 27 29 syl11 ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
31 8 30 biimtrid ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑊 → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
32 6 31 syl ⊢ ( 𝑁 ∈ ℙ → ( 𝑥 ∈ 𝑊 → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
33 32 imp ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) )
34 scshwfzeqfzo ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
35 33 34 syl ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
36 35 eqeq2d ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
37 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑚 ) )
38 37 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
39 38 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
40 eqeq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ 𝑢 = ( 𝑥 cyclShift 𝑚 ) ) )
41 eqcom ⊢ ( 𝑢 = ( 𝑥 cyclShift 𝑚 ) ↔ ( 𝑥 cyclShift 𝑚 ) = 𝑢 )
42 40 41 bitrdi ⊢ ( 𝑦 = 𝑢 → ( 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
43 42 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
44 39 43 bitrid ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
45 44 cbvrabv ⊢ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 }
46 45 cshwshash ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ∨ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ) )
47 46 adantr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ∧ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ∨ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ) )
48 47 orcomd ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ∧ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ∨ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) )
49 fveqeq2 ⊢ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ↔ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ) )
50 fveqeq2 ⊢ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ↔ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) )
51 49 50 orbi12d ⊢ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ∨ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) ) )
52 51 adantl ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ∧ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = 1 ∨ ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) ) )
53 48 52 mpbird ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ∧ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) )
54 53 ex ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) )
55 54 ex ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
56 55 adantr ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
57 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑁 ∈ ℙ ↔ ( ♯ ‘ 𝑥 ) ∈ ℙ ) )
58 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
59 58 rexeqdv ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )
60 59 rabbidv ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
61 60 eqeq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
62 eqeq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( ♯ ‘ 𝑈 ) = 𝑁 ↔ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) )
63 62 orbi2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ↔ ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) )
64 61 63 imbi12d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ↔ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
65 57 64 imbi12d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
66 65 eqcoms ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
67 66 adantl ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
68 56 67 mpbird ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) )
69 29 68 syl ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) )
70 69 1 eleq2s ⊢ ( 𝑥 ∈ 𝑊 → ( 𝑁 ∈ ℙ → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) )
71 70 impcom ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
72 36 71 sylbid ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
73 13 72 sylbid ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
74 73 rexlimdva ⊢ ( 𝑁 ∈ ℙ → ( ∃ 𝑥 ∈ 𝑊 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
75 74 com12 ⊢ ( ∃ 𝑥 ∈ 𝑊 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( 𝑁 ∈ ℙ → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
76 3 75 biimtrdi ⊢ ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( 𝑁 ∈ ℙ → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) )
77 76 pm2.43i ⊢ ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( 𝑁 ∈ ℙ → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
78 77 impcom ⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑈 ∈ ( 𝑊 / ∼ ) ) → ( ( ♯ ‘ 𝑈 ) = 1 ∨ ( ♯ ‘ 𝑈 ) = 𝑁 ) )