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

Theorem wwlksext2clwwlk 26807
Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.)
Hypotheses
Ref Expression
clwwlksext2edg.v 𝑉 = (Vtx‘𝐺)
clwwlksext2edg.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
wwlksext2clwwlk ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍𝑉𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))

Proof of Theorem wwlksext2clwwlk
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 clwwlksext2edg.v . . . 4 𝑉 = (Vtx‘𝐺)
21wwlknbp 26619 . . 3 (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉))
3 simp3 1061 . . . . . . . . 9 ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉)
43adantr 481 . . . . . . . 8 (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → 𝑊 ∈ Word 𝑉)
5 s1cl 13329 . . . . . . . . 9 (𝑍𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
65adantr 481 . . . . . . . 8 ((𝑍𝑉𝑁 ∈ ℕ0) → ⟨“𝑍”⟩ ∈ Word 𝑉)
7 ccatcl 13306 . . . . . . . 8 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
84, 6, 7syl2an 494 . . . . . . 7 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
98adantr 481 . . . . . 6 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
10 clwwlksext2edg.e . . . . . . . . . . . 12 𝐸 = (Edg‘𝐺)
111, 10wwlknp 26620 . . . . . . . . . . 11 (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
12 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉)
1312adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉)
146ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
15 elfzo0 12457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁))
16 simp1 1059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0)
17 peano2nn 10984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
18173ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ)
19 nn0re 11253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ℕ0𝑖 ∈ ℝ)
20193ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ)
21 nnre 10979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
22213ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ)
23 peano2re 10161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
2421, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25243ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ)
26 simp3 1061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < 𝑁)
2721ltp1d 10906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
28273ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1))
2920, 22, 25, 26, 28lttrd 10150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1))
30 elfzo0 12457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1)))
3116, 18, 29, 30syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑖 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
3215, 31sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
3332adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
34 oveq2 6618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((#‘𝑊) = (𝑁 + 1) → (0..^(#‘𝑊)) = (0..^(𝑁 + 1)))
3534adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (0..^(#‘𝑊)) = (0..^(𝑁 + 1)))
3635eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
3736adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
3837adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
3933, 38mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(#‘𝑊)))
40 ccatval1 13308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊𝑖))
4113, 14, 39, 40syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊𝑖))
4241eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖))
43 fzonn0p1p1 12495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
4443adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
4534eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑊) = (𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
4645ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(#‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
4744, 46mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(#‘𝑊)))
48 ccatval1 13308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
4913, 14, 47, 48syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
5049eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)))
5142, 50preq12d 4251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))})
5251eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5352ralbidva 2980 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5453biimpd 219 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5554ex 450 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍𝑉𝑁 ∈ ℕ0) → (∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
5655com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ((𝑍𝑉𝑁 ∈ ℕ0) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
57563impia 1258 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑍𝑉𝑁 ∈ ℕ0) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5857com12 32 . . . . . . . . . . . . . . . . 17 ((𝑍𝑉𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
5958adantr 481 . . . . . . . . . . . . . . . 16 (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
6059impcom 446 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
61 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑊) = (𝑁 + 1) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1))
6261ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1))
63 nn0cn 11254 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
6463ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑁 ∈ ℂ)
65 pncan1 10406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁)
6762, 66eqtr2d 2656 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑁 = ((#‘𝑊) − 1))
6867fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁) = ((𝑊 ++ ⟨“𝑍”⟩)‘((#‘𝑊) − 1)))
696adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
70 nn0p1gt0 11274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
7170ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
72 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((#‘𝑊) = (𝑁 + 1) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1)))
7372ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1)))
7471, 73mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 0 < (#‘𝑊))
75 hashneq0 13103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅))
7612, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅))
7774, 76mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅)
78 ccatval1lsw 13315 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((#‘𝑊) − 1)) = ( lastS ‘𝑊))
7912, 69, 77, 78syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((#‘𝑊) − 1)) = ( lastS ‘𝑊))
8068, 79eqtr2d 2656 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ( lastS ‘𝑊) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
81 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 + 1) = (#‘𝑊) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(#‘𝑊)))
8281eqcoms 2629 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑊) = (𝑁 + 1) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(#‘𝑊)))
8382ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(#‘𝑊)))
84 ccatws1ls 13356 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑊 ∈ Word 𝑉𝑍𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(#‘𝑊)) = 𝑍)
8584ad2ant2r 782 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(#‘𝑊)) = 𝑍)
8683, 85eqtr2d 2656 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
8780, 86preq12d 4251 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {( lastS ‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
88873adantl3 1217 . . . . . . . . . . . . . . . . . . 19 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {( lastS ‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
8988eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
9089biimpd 219 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
9190impr 648 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸)
92 simprlr 802 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → 𝑁 ∈ ℕ0)
93 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
94 oveq1 6617 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑁 → (𝑖 + 1) = (𝑁 + 1))
9594fveq2d 6157 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
9693, 95preq12d 4251 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑁 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
9796eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑁 → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
9897ralsng 4194 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0 → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
9992, 98syl 17 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
10091, 99mpbird 247 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
101 ralunb 3777 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
10260, 100, 101sylanbrc 697 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
103 elnn0uz 11677 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
104103biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
105104ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ (ℤ‘0))
106105adantl 482 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → 𝑁 ∈ (ℤ‘0))
107 fzosplitsn 12525 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
108106, 107syl 17 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
109108raleqdv 3136 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
110102, 109mpbird 247 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
111 simp1 1059 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → 𝑊 ∈ Word 𝑉)
112 simpll 789 . . . . . . . . . . . . . . . . . 18 (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → 𝑍𝑉)
113 ccatws1len 13345 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉𝑍𝑉) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = ((#‘𝑊) + 1))
114111, 112, 113syl2an 494 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = ((#‘𝑊) + 1))
115114oveq1d 6625 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (((#‘𝑊) + 1) − 1))
116 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑊) = (𝑁 + 1) → ((#‘𝑊) + 1) = ((𝑁 + 1) + 1))
117116oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑊) = (𝑁 + 1) → (((#‘𝑊) + 1) − 1) = (((𝑁 + 1) + 1) − 1))
118 ax-1cn 9946 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
119 addcl 9970 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 + 1) ∈ ℂ)
120 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → 1 ∈ ℂ)
121119, 120pncand 10345 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
12263, 118, 121sylancl 693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
123117, 122sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ0 ∧ (#‘𝑊) = (𝑁 + 1)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))
124123ex 450 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → ((#‘𝑊) = (𝑁 + 1) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)))
125124ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → ((#‘𝑊) = (𝑁 + 1) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)))
126125com12 32 . . . . . . . . . . . . . . . . . 18 ((#‘𝑊) = (𝑁 + 1) → (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)))
1271263ad2ant2 1081 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1)))
128127imp 445 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (((#‘𝑊) + 1) − 1) = (𝑁 + 1))
129115, 128eqtrd 2655 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 + 1))
130129oveq2d 6626 . . . . . . . . . . . . . 14 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 + 1)))
131130raleqdv 3136 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → (∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
132110, 131mpbird 247 . . . . . . . . . . . 12 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑍𝑉𝑁 ∈ ℕ0) ∧ {( lastS ‘𝑊), 𝑍} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
133132exp32 630 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑍𝑉𝑁 ∈ ℕ0) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
13411, 133syl 17 . . . . . . . . . 10 (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍𝑉𝑁 ∈ ℕ0) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
135134adantl 482 . . . . . . . . 9 (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍𝑉𝑁 ∈ ℕ0) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
136135imp 445 . . . . . . . 8 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
137136adantrd 484 . . . . . . 7 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
138137imp 445 . . . . . 6 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
139 simpll 789 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word 𝑉)
140 simpl 473 . . . . . . . . . . . . . . . . . 18 ((𝑍𝑉𝑁 ∈ ℕ0) → 𝑍𝑉)
141 lswccats1 13357 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉𝑍𝑉) → ( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
142139, 140, 141syl2an 494 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
143142eqcomd 2627 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑍 = ( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)))
144139adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉)
1456adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
14670adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 < (𝑁 + 1))
14772ad2antlr 762 . . . . . . . . . . . . . . . . . . 19 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → (0 < (#‘𝑊) ↔ 0 < (𝑁 + 1)))
148146, 147mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) → 0 < (#‘𝑊))
149148adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → 0 < (#‘𝑊))
150 ccatfv0 13314 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
151150eqcomd 2627 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊‘0) = ((𝑊 ++ ⟨“𝑍”⟩)‘0))
152144, 145, 149, 151syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (𝑊‘0) = ((𝑊 ++ ⟨“𝑍”⟩)‘0))
153143, 152preq12d 4251 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ0) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)})
154153exp31 629 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ0 → ((𝑍𝑉𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)})))
155154com12 32 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍𝑉𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)})))
1561553ad2ant2 1081 . . . . . . . . . . . 12 ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍𝑉𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)})))
157 wwlknbp2 26638 . . . . . . . . . . . . 13 (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)))
1581wrdeqi 13275 . . . . . . . . . . . . . . . . 17 Word 𝑉 = Word (Vtx‘𝐺)
159158eqcomi 2630 . . . . . . . . . . . . . . . 16 Word (Vtx‘𝐺) = Word 𝑉
160159eleq2i 2690 . . . . . . . . . . . . . . 15 (𝑊 ∈ Word (Vtx‘𝐺) ↔ 𝑊 ∈ Word 𝑉)
161160biimpi 206 . . . . . . . . . . . . . 14 (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉)
162161anim1i 591 . . . . . . . . . . . . 13 ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)))
163157, 162syl 17 . . . . . . . . . . . 12 (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)))
164156, 163impel 485 . . . . . . . . . . 11 (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍𝑉𝑁 ∈ ℕ0) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)}))
165164imp 445 . . . . . . . . . 10 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {𝑍, (𝑊‘0)} = {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)})
166165eleq1d 2683 . . . . . . . . 9 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ({𝑍, (𝑊‘0)} ∈ 𝐸 ↔ {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
167166biimpcd 239 . . . . . . . 8 ({𝑍, (𝑊‘0)} ∈ 𝐸 → ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
168167adantl 482 . . . . . . 7 (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
169168impcom 446 . . . . . 6 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸)
1709, 138, 1693jca 1240 . . . . 5 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
171113ad2ant2r 782 . . . . . . . . . . 11 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = ((#‘𝑊) + 1))
172116adantl 482 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) + 1) = ((𝑁 + 1) + 1))
173 1cnd 10008 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
17463, 173, 173addassd 10014 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
175 1p1e2 11086 . . . . . . . . . . . . . . 15 (1 + 1) = 2
176175oveq2i 6621 . . . . . . . . . . . . . 14 (𝑁 + (1 + 1)) = (𝑁 + 2)
177174, 176syl6eq 2671 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + 2))
178177adantl 482 . . . . . . . . . . . 12 ((𝑍𝑉𝑁 ∈ ℕ0) → ((𝑁 + 1) + 1) = (𝑁 + 2))
179172, 178sylan9eq 2675 . . . . . . . . . . 11 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → ((#‘𝑊) + 1) = (𝑁 + 2))
180171, 179eqtrd 2655 . . . . . . . . . 10 (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
181180ex 450 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑍𝑉𝑁 ∈ ℕ0) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2)))
182163, 181syl 17 . . . . . . . 8 (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍𝑉𝑁 ∈ ℕ0) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2)))
183182adantl 482 . . . . . . 7 (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍𝑉𝑁 ∈ ℕ0) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2)))
184183imp 445 . . . . . 6 ((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
185184adantr 481 . . . . 5 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
186 2nn 11137 . . . . . . . . 9 2 ∈ ℕ
187 nn0nnaddcl 11276 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ)
188186, 187mpan2 706 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 2) ∈ ℕ)
1891883ad2ant2 1081 . . . . . . 7 ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) → (𝑁 + 2) ∈ ℕ)
1901, 10isclwwlksnx 26773 . . . . . . 7 ((𝑁 + 2) ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
191189, 190syl 17 . . . . . 6 ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
192191ad3antrrr 765 . . . . 5 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (#‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
193170, 185, 192mpbir2and 956 . . . 4 (((((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) ∧ (𝑍𝑉𝑁 ∈ ℕ0)) ∧ ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
194193exp31 629 . . 3 (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0𝑊 ∈ Word 𝑉) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺)) → ((𝑍𝑉𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
1952, 194mpancom 702 . 2 (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑍𝑉𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
1961953impib 1259 1 ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍𝑉𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  Vcvv 3189  cun 3557  c0 3896  {csn 4153  {cpr 4155   class class class wbr 4618  cfv 5852  (class class class)co 6610  cc 9886  cr 9887  0cc0 9888  1c1 9889   + caddc 9891   < clt 10026  cmin 10218  cn 10972  2c2 11022  0cn0 11244  cuz 11639  ..^cfzo 12414  #chash 13065  Word cword 13238   lastS clsw 13239   ++ cconcat 13240  ⟨“cs1 13241  Vtxcvtx 25791  Edgcedg 25856   WWalksN cwwlksn 26604   ClWWalksN cclwwlksn 26760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-card 8717  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-2 11031  df-n0 11245  df-xnn0 11316  df-z 11330  df-uz 11640  df-rp 11785  df-fz 12277  df-fzo 12415  df-hash 13066  df-word 13246  df-lsw 13247  df-concat 13248  df-s1 13249  df-wwlks 26608  df-wwlksn 26609  df-clwwlks 26761  df-clwwlksn 26762
This theorem is referenced by:  numclwwlk2lem1  27107
  Copyright terms: Public domain W3C validator