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 41221
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 790 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 𝑃 ∈ Word (Vtx‘𝐺))
2 fstwrdne0 13200 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) ∈ (Vtx‘𝐺))
3 ccatws1n0 13261 . . . . . 6 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
41, 2, 3syl2anc 691 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
543adant3 1074 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅)
6 simp2l 1080 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → 𝑃 ∈ Word (Vtx‘𝐺))
72s1cld 13236 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
873adant3 1074 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
9 ccatcl 13212 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺)) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺))
106, 8, 9syl2anc 691 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺))
111adantr 480 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑃 ∈ Word (Vtx‘𝐺))
127adantr 480 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺))
13 elfzonn0 12380 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ ℕ0)
1413adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ ℕ0)
15 nnz 11276 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1615adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ ℤ)
17 elfzo0 12376 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0..^(𝑁 − 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧ 𝑖 < (𝑁 − 1)))
18 nn0re 11178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
1918adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → 𝑖 ∈ ℝ)
20 nnre 10904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
21 peano2rem 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
2220, 21syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
2322adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℝ)
2420adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
2519, 23, 243jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ))
2625adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ))
27 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → 𝑖 < (𝑁 − 1))
2820ltm1d 10835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
2928adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁)
3029adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → (𝑁 − 1) < 𝑁)
31 lttr 9993 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁) → 𝑖 < 𝑁))
3231imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁)) → 𝑖 < 𝑁)
3326, 27, 30, 32syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑖 ∈ ℕ0𝑁 ∈ ℕ) ∧ 𝑖 < (𝑁 − 1)) → 𝑖 < 𝑁)
3433ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ) → (𝑖 < (𝑁 − 1) → 𝑖 < 𝑁))
3534impancom 455 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℕ0𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
36353adant2 1073 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
3717, 36sylbi 206 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0..^(𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁))
3837impcom 445 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 < 𝑁)
39 elfzo0z 12377 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
4014, 16, 38, 39syl3anbrc 1239 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
4140adantlr 747 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁))
42 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 ((#‘𝑃) = 𝑁 → (0..^(#‘𝑃)) = (0..^𝑁))
4342eleq2d 2673 . . . . . . . . . . . . . . . . . 18 ((#‘𝑃) = 𝑁 → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4443ad2antll 761 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4544adantr 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁)))
4641, 45mpbird 246 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^(#‘𝑃)))
47 ccatval1 13214 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = (𝑃𝑖))
4811, 12, 46, 47syl3anc 1318 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = (𝑃𝑖))
4948eqcomd 2616 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃𝑖) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖))
50 elfzom1p1elfzo 12414 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
5150adantlr 747 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁))
5242ad2antll 761 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0..^(#‘𝑃)) = (0..^𝑁))
5352adantr 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (0..^(#‘𝑃)) = (0..^𝑁))
5451, 53eleqtrrd 2691 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝑃)))
55 ccatval1 13214 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ (𝑖 + 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
5611, 12, 54, 55syl3anc 1318 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
5756eqcomd 2616 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)))
5849, 57preq12d 4220 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑃𝑖), (𝑃‘(𝑖 + 1))} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))})
5958eleq1d 2672 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6059ralbidva 2968 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6160biimpcd 238 . . . . . . . . 9 (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6261adantr 480 . . . . . . . 8 ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
6362expdcom 454 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
64633imp 1249 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
65 fzo0end 12426 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
6665adantr 480 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^𝑁))
6742eleq2d 2673 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = 𝑁 → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁)))
6867ad2antll 761 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁)))
6966, 68mpbird 246 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^(#‘𝑃)))
70 ccatval1 13214 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1)))
711, 7, 69, 70syl3anc 1318 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1)))
72 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑁 = (#‘𝑃) → (𝑁 − 1) = ((#‘𝑃) − 1))
7372fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑁 = (#‘𝑃) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
7473eqcoms 2618 . . . . . . . . . . . . . . . . 17 ((#‘𝑃) = 𝑁 → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
7574adantl 481 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1)))
76 lsw 13204 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
7776adantr 480 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1)))
7875, 77eqtr4d 2647 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃))
7978adantl 481 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃))
8071, 79eqtr2d 2645 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘𝑃) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)))
81 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑁 = (#‘𝑃) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
8281eqcoms 2618 . . . . . . . . . . . . . . 15 ((#‘𝑃) = 𝑁 → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
8382ad2antll 761 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)))
84 nncn 10905 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
85 1cnd 9935 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 1 ∈ ℂ)
8684, 85npcand 10275 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
8786eqcomd 2616 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 = ((𝑁 − 1) + 1))
8887fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
8988adantr 480 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑁) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
90 ccatws1ls 13262 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)) = (𝑃‘0))
911, 2, 90syl2anc 691 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(#‘𝑃)) = (𝑃‘0))
9283, 89, 913eqtr3rd 2653 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
9380, 92preq12d 4220 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {( lastS ‘𝑃), (𝑃‘0)} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))})
9493eleq1d 2672 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9594biimpcd 238 . . . . . . . . . 10 ({( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9695adantl 481 . . . . . . . . 9 ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
9796expdcom 454 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))))
98973imp 1249 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
99 ovex 6577 . . . . . . . 8 (𝑁 − 1) ∈ V
100 fveq2 6103 . . . . . . . . . 10 (𝑖 = (𝑁 − 1) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)))
101 oveq1 6556 . . . . . . . . . . 11 (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1))
102101fveq2d 6107 . . . . . . . . . 10 (𝑖 = (𝑁 − 1) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1)))
103100, 102preq12d 4220 . . . . . . . . 9 (𝑖 = (𝑁 − 1) → {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} = {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))})
104103eleq1d 2672 . . . . . . . 8 (𝑖 = (𝑁 − 1) → ({((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺)))
10599, 104ralsn 4169 . . . . . . 7 (∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑁 − 1)), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘((𝑁 − 1) + 1))} ∈ (Edg‘𝐺))
10698, 105sylibr 223 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
10784, 85, 85addsubd 10292 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = ((𝑁 − 1) + 1))
108107oveq2d 6565 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = (0..^((𝑁 − 1) + 1)))
109 nnm1nn0 11211 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
110 elnn0uz 11601 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (ℤ‘0))
111109, 110sylib 207 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘0))
112 fzosplitsn 12442 . . . . . . . . . . 11 ((𝑁 − 1) ∈ (ℤ‘0) → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
113111, 112syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
114108, 113eqtrd 2644 . . . . . . . . 9 (𝑁 ∈ ℕ → (0..^((𝑁 + 1) − 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}))
115114raleqdv 3121 . . . . . . . 8 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
116 ralunb 3756 . . . . . . . 8 (∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
117115, 116syl6bb 275 . . . . . . 7 (𝑁 ∈ ℕ → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
1181173ad2ant1 1075 . . . . . 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 959 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
120 ccatlen 13213 . . . . . . . . . . 11 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)))
1211, 7, 120syl2anc 691 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)))
122 id 22 . . . . . . . . . . . 12 ((#‘𝑃) = 𝑁 → (#‘𝑃) = 𝑁)
123 s1len 13238 . . . . . . . . . . . . 13 (#‘⟨“(𝑃‘0)”⟩) = 1
124123a1i 11 . . . . . . . . . . . 12 ((#‘𝑃) = 𝑁 → (#‘⟨“(𝑃‘0)”⟩) = 1)
125122, 124oveq12d 6567 . . . . . . . . . . 11 ((#‘𝑃) = 𝑁 → ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
126125ad2antll 761 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((#‘𝑃) + (#‘⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
127121, 126eqtrd 2644 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
1281273adant3 1074 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))
129128oveq1d 6564 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1) = ((𝑁 + 1) − 1))
130129oveq2d 6565 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)) = (0..^((𝑁 + 1) − 1)))
131130raleqdv 3121 . . . . 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 246 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))
1335, 10, 1323jca 1235 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
134 nnnn0 11176 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
135 iswwlksn 41041 . . . . . 6 (𝑁 ∈ ℕ0 → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
136134, 135syl 17 . . . . 5 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
137 eqid 2610 . . . . . . . 8 (Vtx‘𝐺) = (Vtx‘𝐺)
138 eqid 2610 . . . . . . . 8 (Edg‘𝐺) = (Edg‘𝐺)
139137, 138iswwlks 41039 . . . . . . 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 737 . . . . 5 (𝑁 ∈ ℕ → (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (WWalkS‘𝐺) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1)) ↔ (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
142136, 141bitrd 267 . . . 4 (𝑁 ∈ ℕ → ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ↔ (((𝑃 ++ ⟨“(𝑃‘0)”⟩) ≠ ∅ ∧ (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) − 1)){((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘𝑖), ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑁 + 1))))
1431423ad2ant1 1075 . . 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 959 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺))
145 lswccats1 13263 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑃‘0))
1461, 2, 145syl2anc 691 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = (𝑃‘0))
147 lbfzo0 12375 . . . . . . . 8 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
148147biimpri 217 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ (0..^𝑁))
149148adantr 480 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^𝑁))
15042eleq2d 2673 . . . . . . 7 ((#‘𝑃) = 𝑁 → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁)))
151150ad2antll 761 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁)))
152149, 151mpbird 246 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^(#‘𝑃)))
153 ccatval1 13214 . . . . 5 ((𝑃 ∈ Word (Vtx‘𝐺) ∧ ⟨“(𝑃‘0)”⟩ ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(#‘𝑃))) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0) = (𝑃‘0))
1541, 7, 152, 153syl3anc 1318 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0) = (𝑃‘0))
155146, 154eqtr4d 2647 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
1561553adant3 1074 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
157 fveq2 6103 . . . 4 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → ( lastS ‘𝑤) = ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)))
158 fveq1 6102 . . . 4 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → (𝑤‘0) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
159157, 158eqeq12d 2625 . . 3 (𝑤 = (𝑃 ++ ⟨“(𝑃‘0)”⟩) → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0)))
160 clwwlksbij.d . . 3 𝐷 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}
161159, 160elrab2 3333 . 2 ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ 𝐷 ↔ ((𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ (𝑁 WWalkSN 𝐺) ∧ ( lastS ‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0)))
162144, 156, 161sylanbrc 695 1 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ ⟨“(𝑃‘0)”⟩) ∈ 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  {crab 2900  cun 3538  c0 3874  {csn 4125  {cpr 4127   class class class wbr 4583  cfv 5804  (class class class)co 6549  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953  cmin 10145  cn 10897  0cn0 11169  cz 11254  cuz 11563  ..^cfzo 12334  #chash 12979  Word cword 13146   lastS clsw 13147   ++ cconcat 13148  ⟨“cs1 13149  Vtxcvtx 25673  Edgcedga 25792  WWalkScwwlks 41028   WWalkSN cwwlksn 41029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-wwlks 41033  df-wwlksn 41034
This theorem is referenced by:  clwwlksfo  41225  clwwlksnwwlkncl  41228
  Copyright terms: Public domain W3C validator