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 syl5bi ( ( ( ( 𝑥𝑊𝑦𝑊 ) ∧ 𝑧𝑊 ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑛 ∈ ( 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 ( ( 𝑥 𝑦𝑦 𝑧 ) → 𝑥 𝑧 )