Metamath Proof Explorer

Theorem umgrhashecclwwlk

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 equals this length (in an undirected simple graph). (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 umgrhashecclwwlk ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( ♯ ‘ 𝑈 ) = 𝑁 ) )

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 ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
6 prmnn ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ )
7 6 nnnn0d ⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℕ0 )
9 1 eleq2i ⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
10 9 biimpi ⊢ ( 𝑥 ∈ 𝑊 → 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) )
11 clwwlknscsh ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
12 8 10 11 syl2an ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
13 5 12 eqtrd ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
14 13 eqeq2d ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
15 6 adantl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → 𝑁 ∈ ℕ )
16 simpll ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
17 elnnne0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
18 eqeq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑁 = 0 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
19 18 eqcoms ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( 𝑁 = 0 ↔ ( ♯ ‘ 𝑥 ) = 0 ) )
20 hasheq0 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
21 19 20 sylan9bbr ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 = 0 ↔ 𝑥 = ∅ ) )
22 21 necon3bid ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 ≠ 0 ↔ 𝑥 ≠ ∅ ) )
23 22 biimpcd ⊢ ( 𝑁 ≠ 0 → ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑥 ≠ ∅ ) )
24 17 23 simplbiim ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → 𝑥 ≠ ∅ ) )
25 24 impcom ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑥 ≠ ∅ )
26 simplr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ 𝑥 ) = 𝑁 )
27 26 eqcomd ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 = ( ♯ ‘ 𝑥 ) )
28 16 25 27 3jca ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) )
29 28 ex ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑁 ∈ ℕ → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
30 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
31 30 clwwlknbp ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
32 29 31 syl11 ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
33 9 32 syl5bi ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑊 → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
34 15 33 syl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑥 ∈ 𝑊 → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) ) )
35 34 imp ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) )
36 scshwfzeqfzo ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑥 ) ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
37 35 36 syl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
38 37 eqeq2d ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
39 fveq2 ⊢ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
40 simprl ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → 𝐺 ∈ UMGraph )
41 prmuz2 ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℙ → ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 2 ) )
42 41 adantl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 2 ) )
43 42 adantl ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 2 ) )
44 simplr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) )
45 umgr2cwwkdifex ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) ≠ ( 𝑥 ‘ 0 ) )
46 40 43 44 45 syl3anc ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) ≠ ( 𝑥 ‘ 0 ) )
47 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑚 ) )
48 47 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
50 eqeq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ 𝑢 = ( 𝑥 cyclShift 𝑚 ) ) )
51 eqcom ⊢ ( 𝑢 = ( 𝑥 cyclShift 𝑚 ) ↔ ( 𝑥 cyclShift 𝑚 ) = 𝑢 )
52 50 51 bitrdi ⊢ ( 𝑦 = 𝑢 → ( 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
53 52 rexbidv ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
54 49 53 syl5bb ⊢ ( 𝑦 = 𝑢 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 ) )
55 54 cbvrabv ⊢ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑢 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 cyclShift 𝑚 ) = 𝑢 }
56 55 cshwshashnsame ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) ≠ ( 𝑥 ‘ 0 ) → ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) )
57 56 ad2ant2rl ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) ≠ ( 𝑥 ‘ 0 ) → ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) ) )
58 46 57 mpd ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) → ( ♯ ‘ { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) = ( ♯ ‘ 𝑥 ) )
59 39 58 sylan9eqr ⊢ ( ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) ∧ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) ∧ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) )
60 59 exp41 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
61 60 adantr ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
62 oveq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑁 ClWWalksN 𝐺 ) = ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) )
63 62 eleq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) ) )
64 eleq1 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑁 ∈ ℙ ↔ ( ♯ ‘ 𝑥 ) ∈ ℙ ) )
65 64 anbi2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ↔ ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) ) )
66 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
67 66 rexeqdv ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )
68 67 rabbidv ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } )
69 68 eqeq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ↔ 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } ) )
70 eqeq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( ♯ ‘ 𝑈 ) = 𝑁 ↔ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) )
71 69 70 imbi12d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ↔ ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) )
72 65 71 imbi12d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ↔ ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) )
73 63 72 imbi12d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
74 73 eqcoms ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
75 74 adantl ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) ↔ ( 𝑥 ∈ ( ( ♯ ‘ 𝑥 ) ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ ( ♯ ‘ 𝑥 ) ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ 𝑥 ) ) ) ) ) )
76 61 75 mpbird ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) ) )
77 31 76 mpcom ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
78 77 1 eleq2s ⊢ ( 𝑥 ∈ 𝑊 → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
79 78 impcom ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
80 38 79 sylbid ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
81 14 80 sylbid ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
82 81 rexlimdva ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( ∃ 𝑥 ∈ 𝑊 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
83 82 com12 ⊢ ( ∃ 𝑥 ∈ 𝑊 𝑈 = { 𝑦 ∈ 𝑊 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) } → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
84 3 83 syl6bi ⊢ ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑈 ) = 𝑁 ) ) )
85 84 pm2.43i ⊢ ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( ♯ ‘ 𝑈 ) = 𝑁 ) )
86 85 com12 ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ ) → ( 𝑈 ∈ ( 𝑊 / ∼ ) → ( ♯ ‘ 𝑈 ) = 𝑁 ) )