MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwwlkinwwlk Structured version   Visualization version   GIF version

Theorem clwwlkinwwlk 27199
Description: If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 23-Jan-2022.) (Proof shortened by AV, 23-Mar-2022.)
Assertion
Ref Expression
clwwlkinwwlk (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))

Proof of Theorem clwwlkinwwlk
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 eqid 2817 . . 3 (Vtx‘𝐺) = (Vtx‘𝐺)
2 eqid 2817 . . 3 (Edg‘𝐺) = (Edg‘𝐺)
31, 2wwlknp 26974 . 2 (𝑊 ∈ (𝑀 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
4 swrdcl 13649 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
54adantr 468 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
65adantr 468 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺))
7 simpll 774 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑊 ∈ Word (Vtx‘𝐺))
8 simprl 778 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℕ)
9 eluz2 11917 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀))
10 zre 11654 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
11 zre 11654 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
12 id 22 . . . . . . . . . . . . . . . . 17 (𝑁𝑀𝑁𝑀)
1310, 11, 123anim123i 1183 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁𝑀) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
149, 13sylbi 208 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ𝑁) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀))
15 letrp1 11157 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁𝑀) → 𝑁 ≤ (𝑀 + 1))
1614, 15syl 17 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ𝑁) → 𝑁 ≤ (𝑀 + 1))
1716adantl 469 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ≤ (𝑀 + 1))
1817adantl 469 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (𝑀 + 1))
19 breq2 4859 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2019ad2antlr 709 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ≤ (♯‘𝑊) ↔ 𝑁 ≤ (𝑀 + 1)))
2118, 20mpbird 248 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ≤ (♯‘𝑊))
22 swrdn0 13661 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝑊)) → (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅)
237, 8, 21, 22syl3anc 1483 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅)
246, 23jca 503 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
25243adantl3 1202 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
2625adantr 468 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅))
27 nnz 11672 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
28 1nn0 11582 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
29 eluzmn 11918 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ 1 ∈ ℕ0) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
3027, 28, 29sylancl 576 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
31 uzss 11932 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (ℤ𝑁) ⊆ (ℤ‘(𝑁 − 1)))
3332sselda 3809 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ‘(𝑁 − 1)))
34 fzoss2 12727 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
3533, 34syl 17 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
36353ad2ant3 1158 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑀))
37 ssralv 3874 . . . . . . . . . . . . 13 ((0..^(𝑁 − 1)) ⊆ (0..^𝑀) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
3836, 37syl 17 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
39383exp 1141 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
4039com34 91 . . . . . . . . . 10 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
41403imp1 1449 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
4241adantr 468 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))
43 nnnn0 11573 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
44 elnn0uz 11950 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
4543, 44sylib 209 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
46 eluzfz 12567 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ (ℤ‘0) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
4745, 46sylan 571 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...𝑀))
48 fzelp1 12623 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (0...𝑀) → 𝑁 ∈ (0...(𝑀 + 1)))
4947, 48syl 17 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (0...(𝑀 + 1)))
5049adantl 469 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
51 oveq2 6889 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑊) = (𝑀 + 1) → (0...(♯‘𝑊)) = (0...(𝑀 + 1)))
5251eleq2d 2882 . . . . . . . . . . . . . . . . 17 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5352ad2antlr 709 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (0...(♯‘𝑊)) ↔ 𝑁 ∈ (0...(𝑀 + 1))))
5450, 53mpbird 248 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
55 swrd0len 13652 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
567, 54, 55syl2anc 575 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
5756oveq1d 6896 . . . . . . . . . . . . 13 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → ((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1) = (𝑁 − 1))
5857oveq2d 6897 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)) = (0..^(𝑁 − 1)))
5958raleqdv 3344 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
607adantr 468 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑊 ∈ Word (Vtx‘𝐺))
6154adantr 468 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ (0...(♯‘𝑊)))
6230ad2antrl 710 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
63 fzoss2 12727 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
6564sselda 3809 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
66 swrd0fv 13670 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑊𝑖))
6760, 61, 65, 66syl3anc 1483 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 substr ⟨0, 𝑁⟩)‘𝑖) = (𝑊𝑖))
6827ad2antrl 710 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ ℤ)
69 elfzom1elp1fzo 12766 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
7068, 69sylan 571 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
71 swrd0fv 13670 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^𝑁)) → ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7260, 61, 70, 71syl3anc 1483 . . . . . . . . . . . . . 14 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
7367, 72preq12d 4478 . . . . . . . . . . . . 13 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} = {(𝑊𝑖), (𝑊‘(𝑖 + 1))})
7473eleq1d 2881 . . . . . . . . . . . 12 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7574ralbidva 3184 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7659, 75bitrd 270 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
77763adantl3 1202 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7877adantr 468 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7942, 78mpbird 248 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
80 elfz1uz 12640 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...𝑀))
81 fzelp1 12623 . . . . . . . . . . . . . 14 (𝑁 ∈ (1...𝑀) → 𝑁 ∈ (1...(𝑀 + 1)))
8280, 81syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑁 ∈ (1...(𝑀 + 1)))
8382adantl 469 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(𝑀 + 1)))
84 oveq2 6889 . . . . . . . . . . . . . 14 ((♯‘𝑊) = (𝑀 + 1) → (1...(♯‘𝑊)) = (1...(𝑀 + 1)))
8584eleq2d 2882 . . . . . . . . . . . . 13 ((♯‘𝑊) = (𝑀 + 1) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8685ad2antlr 709 . . . . . . . . . . . 12 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 ∈ (1...(♯‘𝑊)) ↔ 𝑁 ∈ (1...(𝑀 + 1))))
8783, 86mpbird 248 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (1...(♯‘𝑊)))
88 swrd0fvlsw 13674 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 substr ⟨0, 𝑁⟩)) = (𝑊‘(𝑁 − 1)))
89 swrd0fv0 13671 . . . . . . . . . . . 12 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 substr ⟨0, 𝑁⟩)‘0) = (𝑊‘0))
9088, 89preq12d 4478 . . . . . . . . . . 11 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(♯‘𝑊))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
917, 87, 90syl2anc 575 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
92913adantl3 1202 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
9392adantr 468 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
94 fz1fzo0m1 12747 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (1...𝑀) → (𝑁 − 1) ∈ (0..^𝑀))
9580, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑁 − 1) ∈ (0..^𝑀))
96953ad2ant3 1158 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑁 − 1) ∈ (0..^𝑀))
97 simpr 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → 𝑖 = (𝑁 − 1))
9897fveq2d 6419 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊𝑖) = (𝑊‘(𝑁 − 1)))
99 oveq1 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
100 nncn 11320 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
101 npcan1 10747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
10399, 102sylan9eqr 2873 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑖 + 1) = 𝑁)
104103fveq2d 6419 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊𝑁))
10598, 104preq12d 4478 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊𝑁)})
106105eleq1d 2881 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
107106ex 399 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
108107adantr 468 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
1091083ad2ant3 1158 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑖 = (𝑁 − 1) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))))
110109imp 395 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
11196, 110rspcdv 3516 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))
1121113exp 1141 . . . . . . . . . . . 12 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
113112com34 91 . . . . . . . . . . 11 (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = (𝑀 + 1) → (∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺)))))
1141133imp1 1449 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
115114adantr 468 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺))
116 preq2 4471 . . . . . . . . . . 11 ((𝑊𝑁) = (𝑊‘0) → {(𝑊‘(𝑁 − 1)), (𝑊𝑁)} = {(𝑊‘(𝑁 − 1)), (𝑊‘0)})
117116eleq1d 2881 . . . . . . . . . 10 ((𝑊𝑁) = (𝑊‘0) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
118117adantl 469 . . . . . . . . 9 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → ({(𝑊‘(𝑁 − 1)), (𝑊𝑁)} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺)))
119115, 118mpbid 223 . . . . . . . 8 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(𝑊‘(𝑁 − 1)), (𝑊‘0)} ∈ (Edg‘𝐺))
12093, 119eqeltrd 2896 . . . . . . 7 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺))
12126, 79, 1203jca 1151 . . . . . 6 ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
122121exp31 408 . . . . 5 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → ((𝑊𝑁) = (𝑊‘0) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))))
1231223imp21 1134 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
1241, 2isclwwlk 27137 . . . 4 ((𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 substr ⟨0, 𝑁⟩) ∈ Word (Vtx‘𝐺) ∧ (𝑊 substr ⟨0, 𝑁⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 substr ⟨0, 𝑁⟩)) − 1)){((𝑊 substr ⟨0, 𝑁⟩)‘𝑖), ((𝑊 substr ⟨0, 𝑁⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑊 substr ⟨0, 𝑁⟩)), ((𝑊 substr ⟨0, 𝑁⟩)‘0)} ∈ (Edg‘𝐺)))
125123, 124sylibr 225 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺))
12647adantl 469 . . . . . . . . . . 11 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...𝑀))
127126, 48syl 17 . . . . . . . . . 10 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(𝑀 + 1)))
128127, 53mpbird 248 . . . . . . . . 9 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → 𝑁 ∈ (0...(♯‘𝑊)))
1297, 128jca 503 . . . . . . . 8 (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) ∧ (𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
130129ex 399 . . . . . . 7 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
1311303adant3 1155 . . . . . 6 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊)))))
132131impcom 396 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1331323adant3 1155 . . . 4 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
134133, 55syl 17 . . 3 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁)
135 isclwwlkn 27183 . . 3 ((𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 substr ⟨0, 𝑁⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝑊 substr ⟨0, 𝑁⟩)) = 𝑁))
136125, 134, 135sylanbrc 574 . 2 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑀 + 1) ∧ ∀𝑖 ∈ (0..^𝑀){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
1373, 136syl3an2 1196 1 (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊𝑁) = (𝑊‘0)) → (𝑊 substr ⟨0, 𝑁⟩) ∈ (𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wne 2989  wral 3107  wss 3780  c0 4127  {cpr 4383  cop 4387   class class class wbr 4855  cfv 6108  (class class class)co 6881  cc 10226  cr 10227  0cc0 10228  1c1 10229   + caddc 10231  cle 10367  cmin 10558  cn 11312  0cn0 11566  cz 11650  cuz 11911  ...cfz 12556  ..^cfzo 12696  chash 13344  Word cword 13509  lastSclsw 13510   substr csubstr 13513  Vtxcvtx 26098  Edgcedg 26163   WWalksN cwwlksn 26957  ClWWalkscclwwlk 27134   ClWWalksN cclwwlkn 27177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-om 7303  df-1st 7405  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-oadd 7807  df-er 7986  df-map 8101  df-pm 8102  df-en 8200  df-dom 8201  df-sdom 8202  df-fin 8203  df-card 9055  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-sub 10560  df-neg 10561  df-nn 11313  df-n0 11567  df-z 11651  df-uz 11912  df-fz 12557  df-fzo 12697  df-hash 13345  df-word 13517  df-lsw 13518  df-substr 13521  df-wwlks 26961  df-wwlksn 26962  df-clwwlk 27135  df-clwwlkn 27179
This theorem is referenced by:  clwwnrepclwwn  27531
  Copyright terms: Public domain W3C validator