This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erclwwlkntr

Description: .~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypotheses erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion erclwwlkntr ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 vex ⊢ 𝑧 ∈ V
6 1 2 erclwwlkneqlen ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
7 6 3adant3 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
8 1 2 erclwwlkneqlen ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ) )
9 8 3adant1 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ) )
10 1 2 erclwwlkneq ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) )
11 10 3adant1 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) )
12 1 2 erclwwlkneq ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
13 12 3adant3 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
14 simpr1 ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → 𝑥 ∈ 𝑊 )
15 simplr2 ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → 𝑧 ∈ 𝑊 )
16 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑦 cyclShift 𝑛 ) = ( 𝑦 cyclShift 𝑚 ) )
17 16 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 = ( 𝑦 cyclShift 𝑛 ) ↔ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) )
18 17 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) )
19 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑧 cyclShift 𝑛 ) = ( 𝑧 cyclShift 𝑘 ) )
20 19 eqeq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑦 = ( 𝑧 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) )
21 20 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ↔ ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) )
22 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 22 clwwlknbp ⊢ ( 𝑧 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑧 ) = 𝑁 ) )
24 eqcom ⊢ ( ( ♯ ‘ 𝑧 ) = 𝑁 ↔ 𝑁 = ( ♯ ‘ 𝑧 ) )
25 24 biimpi ⊢ ( ( ♯ ‘ 𝑧 ) = 𝑁 → 𝑁 = ( ♯ ‘ 𝑧 ) )
26 23 25 simpl2im ⊢ ( 𝑧 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 = ( ♯ ‘ 𝑧 ) )
27 26 1 eleq2s ⊢ ( 𝑧 ∈ 𝑊 → 𝑁 = ( ♯ ‘ 𝑧 ) )
28 27 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → 𝑁 = ( ♯ ‘ 𝑧 ) )
29 23 simpld ⊢ ( 𝑧 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
30 29 1 eleq2s ⊢ ( 𝑧 ∈ 𝑊 → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
31 30 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
32 31 adantl ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
33 simprr ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
34 32 33 cshwcsh2id ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
35 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑧 ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑧 ) ) )
36 oveq2 ⊢ ( ( ♯ ‘ 𝑧 ) = ( ♯ ‘ 𝑦 ) → ( 0 ... ( ♯ ‘ 𝑧 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
37 36 eqcoms ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( 0 ... ( ♯ ‘ 𝑧 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
38 37 adantr ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 0 ... ( ♯ ‘ 𝑧 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
39 38 adantl ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 0 ... ( ♯ ‘ 𝑧 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
40 35 39 sylan9eq ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
41 40 eleq2d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) ↔ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) )
42 41 anbi1d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ↔ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) )
43 35 eleq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑧 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) )
44 43 anbi1d ⊢ ( 𝑁 = ( ♯ ‘ 𝑧 ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ↔ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) )
45 44 adantr ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ↔ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) )
46 42 45 anbi12d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) ↔ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) ) )
47 35 rexeqdv ⊢ ( 𝑁 = ( ♯ ‘ 𝑧 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
48 47 adantr ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
49 34 46 48 3imtr4d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑧 ) ∧ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ) → ( ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
50 28 49 mpancom ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
51 50 exp5l ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
52 51 imp41 ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
53 52 rexlimdva ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
54 53 ex ⊢ ( ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
55 54 rexlimdva ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
56 21 55 syl7bi ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
57 18 56 biimtrid ⊢ ( ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ 𝑧 ∈ 𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
58 57 exp31 ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ( 𝑧 ∈ 𝑊 → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
59 58 com15 ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ( 𝑧 ∈ 𝑊 → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
60 59 impcom ⊢ ( ( 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) )
61 60 3adant1 ⊢ ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) )
62 61 impcom ⊢ ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
63 62 com13 ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
64 63 3impia ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
65 64 impcom ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) )
66 14 15 65 3jca ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ( 𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
67 1 2 erclwwlkneq ⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
68 67 3adant2 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
69 66 68 syl5ibrcom ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → 𝑥 ∼ 𝑧 ) )
70 69 exp31 ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → 𝑥 ∼ 𝑧 ) ) ) )
71 70 com24 ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) )
72 71 ex ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
73 72 com4t ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
74 13 73 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
75 74 com25 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) ) )
76 11 75 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) ) )
77 9 76 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) )
78 77 com24 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) ) )
79 7 78 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) )
80 79 impd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 ) )
81 3 4 5 80 mp3an ⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 )