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