Metamath Proof Explorer

Theorem eleclclwwlknlem2

Description: Lemma 2 for eleclclwwlkn . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypothesis erclwwlkn1.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
Assertion eleclclwwlknlem2 ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn1.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 simpl ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
3 2 anim1i ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) )
4 3 adantr ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) )
5 simpr ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) → 𝑋 = ( 𝑥 cyclShift 𝑘 ) )
6 5 adantr ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → 𝑋 = ( 𝑥 cyclShift 𝑘 ) )
7 6 anim1i ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) → ( 𝑋 = ( 𝑥 cyclShift 𝑘 ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) )
8 1 eleclclwwlknlem1 ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( ( 𝑋 = ( 𝑥 cyclShift 𝑘 ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
9 4 7 8 sylc ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) )
10 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11 10 clwwlknbp ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
12 11 1 eleq2s ⊢ ( 𝑥 ∈ 𝑊 → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
13 fznn0sub2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ( 0 ... 𝑁 ) )
14 oveq1 ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) = ( 𝑁 − 𝑘 ) )
15 14 eleq1d ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝑁 − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
16 13 15 syl5ibr ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
17 16 adantl ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
18 12 17 syl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
19 18 adantl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
20 19 com12 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
21 20 adantr ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ) )
22 21 imp ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) )
23 22 adantr ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) )
24 simpr ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) )
25 24 ancomd ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑥 ∈ 𝑊 ∧ 𝑋 ∈ 𝑊 ) )
26 25 adantr ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ( 𝑥 ∈ 𝑊 ∧ 𝑋 ∈ 𝑊 ) )
27 23 26 jca ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ( ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑋 ∈ 𝑊 ) ) )
28 simpll ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
29 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) )
30 29 eleq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
31 30 eqcoms ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
32 31 adantl ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
33 32 biimpa ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
34 28 33 jca ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
35 34 ex ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) )
36 12 35 syl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) )
37 36 adantl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) )
38 37 com12 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) )
39 38 adantr ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) → ( ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) )
40 39 imp ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
41 5 eqcomd ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) → ( 𝑥 cyclShift 𝑘 ) = 𝑋 )
42 41 adantr ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑥 cyclShift 𝑘 ) = 𝑋 )
43 oveq1 ⊢ ( 𝑋 = ( 𝑥 cyclShift 𝑘 ) → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = ( ( 𝑥 cyclShift 𝑘 ) cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) )
44 43 eqcoms ⊢ ( ( 𝑥 cyclShift 𝑘 ) = 𝑋 → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = ( ( 𝑥 cyclShift 𝑘 ) cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) )
45 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) → 𝑘 ∈ ℤ )
46 2cshwid ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 cyclShift 𝑘 ) cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = 𝑥 )
47 45 46 sylan2 ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ( 𝑥 cyclShift 𝑘 ) cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = 𝑥 )
48 44 47 sylan9eqr ⊢ ( ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ ( 𝑥 cyclShift 𝑘 ) = 𝑋 ) → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = 𝑥 )
49 40 42 48 syl2anc ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) = 𝑥 )
50 49 eqcomd ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → 𝑥 = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) )
51 50 anim1i ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ( 𝑥 = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )
52 1 eleclclwwlknlem1 ⊢ ( ( ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ∈ ( 0 ... 𝑁 ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑋 ∈ 𝑊 ) ) → ( ( 𝑥 = ( 𝑋 cyclShift ( ( ♯ ‘ 𝑥 ) − 𝑘 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ) )
53 27 51 52 sylc ⊢ ( ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) )
54 9 53 impbida ⊢ ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑋 = ( 𝑥 cyclShift 𝑘 ) ) ∧ ( 𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑥 cyclShift 𝑚 ) ↔ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑌 = ( 𝑋 cyclShift 𝑛 ) ) )