Metamath Proof Explorer

Theorem crctcshwlkn0

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

Ref Expression
Hypotheses crctcsh.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
crctcsh.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion crctcshwlkn0 ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )

Proof

Step Hyp Ref Expression
1 crctcsh.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
4 crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
5 crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
6 crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
7 crctcsh.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
8 crctiswlk ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9 2 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
10 cshwcl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 𝐹 cyclShift 𝑆 ) ∈ Word dom 𝐼 )
11 3 8 9 10 4syl ⊢ ( 𝜑 → ( 𝐹 cyclShift 𝑆 ) ∈ Word dom 𝐼 )
12 6 11 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ Word dom 𝐼 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝐻 ∈ Word dom 𝐼 )
14 3 8 syl ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
15 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
16 simpll ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
17 elfznn0 ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℕ0 )
18 17 adantl ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ∈ ℕ0 )
19 elfzonn0 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ ℕ0 )
21 18 20 nn0addcld ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 + 𝑆 ) ∈ ℕ0 )
22 21 adantr ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑥 + 𝑆 ) ∈ ℕ0 )
23 elfz3nn0 ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
24 4 23 eqeltrrid ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
25 24 ad2antlr ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
26 elfzelz ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℤ )
27 26 zred ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℝ )
28 27 adantl ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑥 ∈ ℝ )
29 elfzoelz ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℤ )
30 29 zred ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑆 ∈ ℝ )
31 30 adantr ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ ℝ )
32 elfzel2 ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
33 32 zred ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
34 33 adantl ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
35 leaddsub ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑥 + 𝑆 ) ≤ 𝑁 ↔ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) )
36 28 31 34 35 syl3anc ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑥 + 𝑆 ) ≤ 𝑁 ↔ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) )
37 36 biimpar ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑥 + 𝑆 ) ≤ 𝑁 )
38 37 4 breqtrdi ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑥 + 𝑆 ) ≤ ( ♯ ‘ 𝐹 ) )
39 22 25 38 3jca ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 + 𝑆 ) ≤ ( ♯ ‘ 𝐹 ) ) )
40 5 39 sylanl1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 + 𝑆 ) ≤ ( ♯ ‘ 𝐹 ) ) )
41 elfz2nn0 ⊢ ( ( 𝑥 + 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ ( ( 𝑥 + 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑥 + 𝑆 ) ≤ ( ♯ ‘ 𝐹 ) ) )
42 40 41 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑥 + 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
43 42 adantll ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑥 + 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
44 16 43 ffvelcdmd ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) ∈ 𝑉 )
45 simpll ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
46 elfzoel2 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
47 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝑥 + 𝑆 ) ∈ ℤ )
48 47 adantrr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑥 + 𝑆 ) ∈ ℤ )
49 simprr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
50 48 49 zsubcld ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ )
51 50 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ )
52 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
53 52 ancoms ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝑆 ) ∈ ℤ )
54 53 zred ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝑆 ) ∈ ℝ )
55 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
56 ltnle ⊢ ( ( ( 𝑁 − 𝑆 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑁 − 𝑆 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) )
57 54 55 56 syl2anr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑁 − 𝑆 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) )
58 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
59 58 adantl ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
60 zre ⊢ ( 𝑆 ∈ ℤ → 𝑆 ∈ ℝ )
61 60 adantr ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑆 ∈ ℝ )
62 55 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑥 ∈ ℝ )
63 ltsubadd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑁 − 𝑆 ) < 𝑥 ↔ 𝑁 < ( 𝑥 + 𝑆 ) ) )
64 59 61 62 63 syl2an23an ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑁 − 𝑆 ) < 𝑥 ↔ 𝑁 < ( 𝑥 + 𝑆 ) ) )
65 59 adantl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℝ )
66 48 zred ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑥 + 𝑆 ) ∈ ℝ )
67 65 66 posdifd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 < ( 𝑥 + 𝑆 ) ↔ 0 < ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
68 0red ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 0 ∈ ℝ )
69 50 zred ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℝ )
70 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℝ ) → ( 0 < ( ( 𝑥 + 𝑆 ) − 𝑁 ) → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
71 68 69 70 syl2anc ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 0 < ( ( 𝑥 + 𝑆 ) − 𝑁 ) → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
72 67 71 sylbid ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 < ( 𝑥 + 𝑆 ) → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
73 64 72 sylbid ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑁 − 𝑆 ) < 𝑥 → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
74 57 73 sylbird ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
75 74 imp ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) )
76 51 75 jca ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
77 76 exp31 ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) )
78 77 26 syl11 ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) )
79 29 46 78 syl2anc ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ) )
80 79 imp31 ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
81 elnn0z ⊢ ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℕ0 ↔ ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) )
82 80 81 sylibr ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℕ0 )
83 24 ad2antlr ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
84 elfzo0 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) )
85 elfz2nn0 ⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) )
86 nn0re ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ℝ )
87 86 3ad2ant1 ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 𝑆 ∈ ℝ )
88 nn0re ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ )
89 88 3ad2ant1 ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) → 𝑥 ∈ ℝ )
90 87 89 anim12ci ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) )
91 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
92 91 91 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
93 92 3ad2ant2 ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
94 93 adantr ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
95 90 94 jca ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) )
96 simpr3 ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → 𝑥 ≤ 𝑁 )
97 ltle ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑆 < 𝑁 → 𝑆 ≤ 𝑁 ) )
98 86 91 97 syl2an ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 < 𝑁 → 𝑆 ≤ 𝑁 ) )
99 98 3impia ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) → 𝑆 ≤ 𝑁 )
100 99 adantr ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → 𝑆 ≤ 𝑁 )
101 95 96 100 jca32 ⊢ ( ( ( 𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ≤ 𝑁 ) ) → ( ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) ∧ ( 𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁 ) ) )
102 84 85 101 syl2anb ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) ∧ ( 𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁 ) ) )
103 le2add ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) → ( ( 𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁 ) → ( 𝑥 + 𝑆 ) ≤ ( 𝑁 + 𝑁 ) ) )
104 103 imp ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) ∧ ( 𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁 ) ) → ( 𝑥 + 𝑆 ) ≤ ( 𝑁 + 𝑁 ) )
105 102 104 syl ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥 + 𝑆 ) ≤ ( 𝑁 + 𝑁 ) )
106 66 65 65 3jca ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
107 106 ex ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) )
108 107 26 syl11 ⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) )
109 29 46 108 syl2anc ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ( 0 ... 𝑁 ) → ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ) )
110 109 imp ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
111 lesubadd ⊢ ( ( ( 𝑥 + 𝑆 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ 𝑁 ↔ ( 𝑥 + 𝑆 ) ≤ ( 𝑁 + 𝑁 ) ) )
112 110 111 syl ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ 𝑁 ↔ ( 𝑥 + 𝑆 ) ≤ ( 𝑁 + 𝑁 ) ) )
113 105 112 mpbird ⊢ ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ 𝑁 )
114 113 adantr ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ 𝑁 )
115 114 4 breqtrdi ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ ( ♯ ‘ 𝐹 ) )
116 82 83 115 3jca ⊢ ( ( ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ ( ♯ ‘ 𝐹 ) ) )
117 5 116 sylanl1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ ( ♯ ‘ 𝐹 ) ) )
118 elfz2nn0 ⊢ ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ ( ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ≤ ( ♯ ‘ 𝐹 ) ) )
119 117 118 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
120 119 adantll ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( ( 𝑥 + 𝑆 ) − 𝑁 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
121 45 120 ffvelcdmd ⊢ ( ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) ∧ ¬ 𝑥 ≤ ( 𝑁 − 𝑆 ) ) → ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ∈ 𝑉 )
122 44 121 ifclda ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ∈ 𝑉 )
123 122 exp32 ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ∈ 𝑉 ) ) )
124 15 123 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ∈ 𝑉 ) ) )
125 14 124 mpcom ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 ... 𝑁 ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ∈ 𝑉 ) )
126 125 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ... 𝑁 ) ) → if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) ∈ 𝑉 )
127 126 7 fmptd ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑁 ) ⟶ 𝑉 )
128 1 2 3 4 5 6 crctcshlem2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = 𝑁 )
129 128 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐻 ) ) = ( 0 ... 𝑁 ) )
130 129 feq2d ⊢ ( 𝜑 → ( 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 ↔ 𝑄 : ( 0 ... 𝑁 ) ⟶ 𝑉 ) )
131 127 130 mpbird ⊢ ( 𝜑 → 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 )
133 1 2 wlkprop ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
134 3 8 133 3syl ⊢ ( 𝜑 → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
135 134 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
136 4 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
137 136 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 )
138 137 raleqi ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
139 fzo1fzo0n0 ⊢ ( 𝑆 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ≠ 0 ) )
140 139 simplbi2 ⊢ ( 𝑆 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ≠ 0 → 𝑆 ∈ ( 1 ..^ 𝑁 ) ) )
141 5 140 syl ⊢ ( 𝜑 → ( 𝑆 ≠ 0 → 𝑆 ∈ ( 1 ..^ 𝑁 ) ) )
142 141 imp ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
143 142 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → 𝑆 ∈ ( 1 ..^ 𝑁 ) )
144 simplll ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → 𝐹 ∈ Word dom 𝐼 )
145 wkslem1 ⊢ ( 𝑖 = 𝑘 → ( if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
146 145 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
147 146 bilani ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
148 crctprop ⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
149 136 fveq2i ⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 𝑁 )
150 149 eqeq2i ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) )
151 150 biimpi ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) )
152 151 eqcomd ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
153 152 adantl ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
154 3 148 153 3syl ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
155 154 ad2antrl ⊢ ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
156 155 adantr ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 0 ) )
157 143 7 6 4 144 147 156 crctcshwlkn0lem7 ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
158 128 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ 𝑁 ) )
159 158 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
160 159 ad2antrl ⊢ ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
161 160 adantr ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
162 157 161 mpbird ⊢ ( ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
163 162 ex ⊢ ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
164 138 163 biimtrid ⊢ ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ( 𝜑 ∧ 𝑆 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
165 164 ex ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) ) )
166 165 com23 ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) → ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) ) )
167 166 3impia ⊢ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) } , { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) → ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
168 135 167 mpcom ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) )
169 13 132 168 3jca ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝐻 ∈ Word dom 𝐼 ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) )
170 1 2 3 4 5 6 7 crctcshlem3 ⊢ ( 𝜑 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) )
172 1 2 iswlk ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V ) → ( 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ↔ ( 𝐻 ∈ Word dom 𝐼 ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) ) )
173 171 172 syl ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → ( 𝐻 ( Walks ‘ 𝐺 ) 𝑄 ↔ ( 𝐻 ∈ Word dom 𝐼 ∧ 𝑄 : ( 0 ... ( ♯ ‘ 𝐻 ) ) ⟶ 𝑉 ∧ ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐻 ) ) if- ( ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) , ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) = { ( 𝑄 ‘ 𝑗 ) } , { ( 𝑄 ‘ 𝑗 ) , ( 𝑄 ‘ ( 𝑗 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐻 ‘ 𝑗 ) ) ) ) ) )
174 169 173 mpbird ⊢ ( ( 𝜑 ∧ 𝑆 ≠ 0 ) → 𝐻 ( Walks ‘ 𝐺 ) 𝑄 )