Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clwwlksel Structured version   Visualization version   GIF version

Theorem clwwlksel 41220
Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 25-Apr-2021.)
Hypothesis
Ref Expression
clwwlksbij.d 𝐷 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
Assertion
Ref Expression
clwwlksel ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ 𝐷)
Distinct variable groups:   𝑖,𝐺   𝑤,𝐺   𝑖,𝑁   𝑤,𝑁   𝑃,𝑖   𝑤,𝑃
Allowed substitution hints:   𝐷(𝑤,𝑖)

Proof of Theorem clwwlksel
StepHypRef Expression
1 simprl 789 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 𝑃 ∈ Word (Vtx‘𝐺))
2 fstwrdne0 13143 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) ∈ (Vtx‘𝐺))
3 ccatws1n0 13204 . . . . . 6 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
41, 2, 3syl2anc 690 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
543adant3 1073 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
6 simp2l 1079 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → 𝑃 ∈ Word (Vtx‘𝐺))
72s1cld 13179 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
873adant3 1073 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
9 ccatcl 13155 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺))
106, 8, 9syl2anc 690 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺))
111adantr 479 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑃 ∈ Word (Vtx‘𝐺))
127adantr 479 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
13 elfzonn0 12332 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ ℕ0)
1413adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ ℕ0)
15 nnz 11229 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1615adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ ℤ)
17 elfzo0 12328 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^(𝑁 − 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧ 𝑖 < (𝑁 − 1)))
18 nn0re 11145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
1918adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → 𝑖 ∈ ℝ)
20 nnre 10871 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
21 peano2rem 10196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
2220, 21syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
2322adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℝ)
2420adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
2519, 23, 243jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ))
2625adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ))
27 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → 𝑖 < (𝑁 − 1))
2820ltm1d 10802 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
2928adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁)
3029adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → (𝑁 − 1) < 𝑁)
31 lttr 9962 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁) → 𝑖 < 𝑁))
3231imp 443 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁)) → 𝑖 < 𝑁)
3326, 27, 30, 32syl12anc 1315 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → 𝑖 < 𝑁)
3433ex 448 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑖 < (𝑁 − 1) → 𝑖 < 𝑁))
3534impancom 454 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℕ0𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
36353adant2 1072 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
3717, 36sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^(𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
3837impcom 444 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 < 𝑁)
39 elfzo0z 12329 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
4014, 16, 38, 39syl3anbrc 1238 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
4140adantlr 746 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
42 oveq2 6532 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑃) = 𝑁 → (0..^(#‘𝑃)) = (0..^𝑁))
4342eleq2d 2669 . . . . . . . . . . . . . . . . . 18 ((#‘𝑃) = 𝑁 → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4443ad2antll 760 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4544adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4641, 45mpbird 245 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^(#‘𝑃)))
47 ccatval1 13157 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = (𝑃𝑖))
4811, 12, 46, 47syl3anc 1317 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = (𝑃𝑖))
4948eqcomd 2612 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃𝑖) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖))
50 elfzom1p1elfzo 12366 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
5150adantlr 746 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
5242ad2antll 760 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0..^(#‘𝑃)) = (0..^𝑁))
5352adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (0..^(#‘𝑃)) = (0..^𝑁))
5451, 53eleqtrrd 2687 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝑃)))
55 ccatval1 13157 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
5611, 12, 54, 55syl3anc 1317 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
5756eqcomd 2612 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)))
5849, 57preq12d 4216 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))})
5958eleq1d 2668 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6059ralbidva 2964 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6160biimpcd 237 . . . . . . . . 9 (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6261adantr 479 . . . . . . . 8 ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6362expdcom 453 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
64633imp 1248 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
65 fzo0end 12378 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
6665adantr 479 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^𝑁))
6742eleq2d 2669 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = 𝑁 → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁)))
6867ad2antll 760 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁)))
6966, 68mpbird 245 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^(#‘𝑃)))
70 ccatval1 13157 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1)))
711, 7, 69, 70syl3anc 1317 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1)))
72 oveq1 6531 . . . . . . . . . . . . . . . . . . 19 (𝑁 = (#‘𝑃) → (𝑁 − 1) = ((#‘𝑃) − 1))
7372fveq2d 6089 . . . . . . . . . . . . . . . . . 18 (𝑁 = (#‘𝑃) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
7473eqcoms 2614 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = 𝑁 → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
7574adantl 480 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
76 lsw 13147 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
7776adantr 479 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
7875, 77eqtr4d 2643 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃))
7978adantl 480 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃))
8071, 79eqtr2d 2641 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘𝑃) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)))
81 fveq2 6085 . . . . . . . . . . . . . . . 16 (𝑁 = (#‘𝑃) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
8281eqcoms 2614 . . . . . . . . . . . . . . 15 ((#‘𝑃) = 𝑁 → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
8382ad2antll 760 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
84 nncn 10872 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
85 1cnd 9909 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 1 ∈ ℂ)
8684, 85npcand 10244 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
8786eqcomd 2612 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 = ((𝑁 − 1) + 1))
8887fveq2d 6089 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
8988adantr 479 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
90 ccatws1ls 13205 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)) = (𝑃‘0))
911, 2, 90syl2anc 690 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)) = (𝑃‘0))
9283, 89, 913eqtr3rd 2649 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
9380, 92preq12d 4216 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {( lastS ‘𝑃), (𝑃‘0)} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))})
9493eleq1d 2668 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9594biimpcd 237 . . . . . . . . . 10 ({( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9695adantl 480 . . . . . . . . 9 ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9796expdcom 453 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))))
98973imp 1248 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
99 ovex 6552 . . . . . . . 8 (𝑁 − 1) ∈ V
100 fveq2 6085 . . . . . . . . . 10 (𝑖 = (𝑁 − 1) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)))
101 oveq1 6531 . . . . . . . . . . 11 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
102101fveq2d 6089 . . . . . . . . . 10 (𝑖 = (𝑁 − 1) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
103100, 102preq12d 4216 . . . . . . . . 9 (𝑖 = (𝑁 − 1) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))})
104103eleq1d 2668 . . . . . . . 8 (𝑖 = (𝑁 − 1) → ({((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
10599, 104ralsn 4165 . . . . . . 7 (∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
10698, 105sylibr 222 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
10784, 85, 85addsubd 10261 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
108107oveq2d 6540 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^((𝑁 − 1) + 1)))
109 nnm1nn0 11178 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
110 elnn0uz 11554 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (ℤ‘0))
111109, 110sylib 206 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘0))
112 fzosplitsn 12394 . . . . . . . . . . 11 ((𝑁 − 1) ∈ (ℤ‘0) → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
113111, 112syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
114108, 113eqtrd 2640 . . . . . . . . 9 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
115114raleqdv 3117 . . . . . . . 8 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
116 ralunb 3752 . . . . . . . 8 (∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
117115, 116syl6bb 274 . . . . . . 7 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1181173ad2ant1 1074 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
11964, 106, 118mpbir2and 958 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
120 ccatlen 13156 . . . . . . . . . . 11 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)))
1211, 7, 120syl2anc 690 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)))
122 id 22 . . . . . . . . . . . 12 ((#‘𝑃) = 𝑁 → (#‘𝑃) = 𝑁)
123 s1len 13181 . . . . . . . . . . . . 13 (#‘⟨“(𝑃‘0)”⟩) = 1
124123a1i 11 . . . . . . . . . . . 12 ((#‘𝑃) = 𝑁 → (#‘⟨“(𝑃‘0)”⟩) = 1)
125122, 124oveq12d 6542 . . . . . . . . . . 11 ((#‘𝑃) = 𝑁 → ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
126125ad2antll 760 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
127121, 126eqtrd 2640 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
1281273adant3 1073 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
129128oveq1d 6539 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1) = ((𝑁 + 1) − 1))
130129oveq2d 6540 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)) = (0..^((𝑁 + 1) − 1)))
131130raleqdv 3117 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132119, 131mpbird 245 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
1335, 10, 1323jca 1234 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
134 nnnn0 11143 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
135 iswwlksn 41040 . . . . . 6 (𝑁 ∈ ℕ0 → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
136134, 135syl 17 . . . . 5 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
137 eqid 2606 . . . . . . . 8 (Vtx‘𝐺) = (Vtx‘𝐺)
138 eqid 2606 . . . . . . . 8 (Edg‘𝐺) = (Edg‘𝐺)
139137, 138iswwlks 41038 . . . . . . 7 ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
140139a1i 11 . . . . . 6 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
141140anbi1d 736 . . . . 5 (𝑁 ∈ ℕ → (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1)) ↔ (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
142136, 141bitrd 266 . . . 4 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
1431423ad2ant1 1074 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
144133, 128, 143mpbir2and 958 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺))
145 lswccats1 13206 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑃‘0))
1461, 2, 145syl2anc 690 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑃‘0))
147 lbfzo0 12327 . . . . . . . 8 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
148147biimpri 216 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ (0..^𝑁))
149148adantr 479 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^𝑁))
15042eleq2d 2669 . . . . . . 7 ((#‘𝑃) = 𝑁 → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁)))
151150ad2antll 760 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁)))
152149, 151mpbird 245 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^(#‘𝑃)))
153 ccatval1 13157 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0) = (𝑃‘0))
1541, 7, 152, 153syl3anc 1317 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0) = (𝑃‘0))
155146, 154eqtr4d 2643 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
1561553adant3 1073 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
157 fveq2 6085 . . . 4 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → ( lastS ‘𝑤) = ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)))
158 fveq1 6084 . . . 4 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → (𝑤‘0) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
159157, 158eqeq12d 2621 . . 3 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0)))
160 clwwlksbij.d . . 3 𝐷 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
161159, 160elrab2 3329 . 2 ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ 𝐷 ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0)))
162144, 156, 161sylanbrc 694 1 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776  wral 2892  {crab 2896  cun 3534  c0 3870  {csn 4121  {cpr 4123   class class class wbr 4574  cfv 5787  (class class class)co 6524  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   < clt 9927  cmin 10114  cn 10864  0cn0 11136  cz 11207  cuz 11516  ..^cfzo 12286  #chash 12931  Word cword 13089   lastS clsw 13090   ++ cconcat 13091  ⟨“cs1 13092  Vtxcvtx 40228  Edgcedga 40350  WWalkScwwlks 41027   WWalkSN cwwlksn 41028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-card 8622  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-nn 10865  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-fzo 12287  df-hash 12932  df-word 13097  df-lsw 13098  df-concat 13099  df-s1 13100  df-wwlks 41032  df-wwlksn 41033
This theorem is referenced by:  clwwlksfo  41224  clwwlksnwwlkncl  41227
  Copyright terms: Public domain W3C validator