Proof of Theorem clwwlkel
Step | Hyp | Ref
| Expression |
1 | | simprl 790 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 𝑃 ∈ Word 𝑉) |
2 | | fstwrdne0 13200 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) ∈ 𝑉) |
3 | | ccatws1n0 13261 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘0) ∈ 𝑉) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
4 | 1, 2, 3 | syl2anc 691 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
5 | 4 | 3ad2antl3 1218 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
6 | 5 | 3adant3 1074 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
7 | | simp2l 1080 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → 𝑃 ∈ Word 𝑉) |
8 | 2 | 3ad2antl3 1218 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) ∈ 𝑉) |
9 | 8 | s1cld 13236 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 〈“(𝑃‘0)”〉 ∈ Word 𝑉) |
10 | 9 | 3adant3 1074 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → 〈“(𝑃‘0)”〉 ∈ Word 𝑉) |
11 | | ccatcl 13212 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
12 | 7, 10, 11 | syl2anc 691 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
13 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑃 ∈ Word 𝑉) |
14 | 2 | s1cld 13236 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 〈“(𝑃‘0)”〉 ∈ Word 𝑉) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 〈“(𝑃‘0)”〉 ∈
Word 𝑉) |
16 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ ℕ0) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ ℕ0) |
18 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ ℤ) |
20 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧
𝑖 < (𝑁 − 1))) |
21 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑖 ∈
ℝ) |
23 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
24 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 1) ∈
ℝ) |
27 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℝ) |
28 | 22, 26, 27 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑖 ∈ ℝ
∧ (𝑁 − 1) ∈
ℝ ∧ 𝑁 ∈
ℝ)) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ)) |
30 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → 𝑖 < (𝑁 − 1)) |
31 | 23 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 1) <
𝑁) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → (𝑁 − 1) < 𝑁) |
34 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ) →
((𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁) → 𝑖 < 𝑁)) |
35 | 34 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ) ∧
(𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁)) → 𝑖 < 𝑁) |
36 | 29, 30, 33, 35 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → 𝑖 < 𝑁) |
37 | 36 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑖 < (𝑁 − 1) → 𝑖 < 𝑁)) |
38 | 37 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
39 | 38 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ (𝑁 − 1) ∈
ℕ ∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
40 | 20, 39 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
41 | 40 | impcom 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 < 𝑁) |
42 | | elfzo0z 12377 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁)) |
43 | 17, 19, 41, 42 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
44 | 43 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
45 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑃) = 𝑁 → (0..^(#‘𝑃)) = (0..^𝑁)) |
46 | 45 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) = 𝑁 → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
47 | 46 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
49 | 44, 48 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^(#‘𝑃))) |
50 | | ccatval1 13214 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(#‘𝑃))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = (𝑃‘𝑖)) |
51 | 13, 15, 49, 50 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = (𝑃‘𝑖)) |
52 | 51 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘𝑖) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖)) |
53 | | elfzom1p1elfzo 12414 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
54 | 53 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
55 | 45 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (0..^(#‘𝑃)) = (0..^𝑁)) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (0..^(#‘𝑃)) = (0..^𝑁)) |
57 | 54, 56 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝑃))) |
58 | | ccatval1 13214 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
59 | 13, 15, 57, 58 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
60 | 59 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))) |
61 | 52, 60 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))}) |
62 | 61 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
63 | 62 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
64 | 63 | biimpcd 238 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
65 | 64 | adantr 480 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
66 | 65 | expdcom 454 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
67 | 66 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
68 | 67 | 3imp 1249 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
69 | | fzo0end 12426 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^𝑁)) |
71 | 45 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) = 𝑁 → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁))) |
72 | 71 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁))) |
73 | 70, 72 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^(#‘𝑃))) |
74 | | ccatval1 13214 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ (𝑁 − 1) ∈ (0..^(#‘𝑃))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1))) |
75 | 1, 14, 73, 74 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1))) |
76 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = (#‘𝑃) → (𝑁 − 1) = ((#‘𝑃) − 1)) |
77 | 76 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑃) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
78 | 77 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) = 𝑁 → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
80 | | lsw 13204 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
82 | 79, 81 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃)) |
83 | 82 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃)) |
84 | 75, 83 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘𝑃) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1))) |
85 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑃) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
86 | 85 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑃) = 𝑁 → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
87 | 86 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
88 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
89 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
90 | 88, 89 | npcand 10275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
91 | 90 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 − 1) + 1)) |
92 | 91 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
94 | | ccatws1ls 13262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘0) ∈ 𝑉) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃)) = (𝑃‘0)) |
95 | 1, 2, 94 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃)) = (𝑃‘0)) |
96 | 87, 93, 95 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
97 | 84, 96 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → {( lastS ‘𝑃), (𝑃‘0)} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))}) |
98 | 97 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸)) |
99 | 98 | biimpcd 238 |
. . . . . . . . . . 11
⊢ ({( lastS
‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸)) |
100 | 99 | adantl 481 |
. . . . . . . . . 10
⊢
((∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸)) |
101 | 100 | expdcom 454 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸))) |
102 | 101 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸))) |
103 | 102 | 3imp 1249 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸) |
104 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑁 − 1) ∈
V |
105 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑁 − 1) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1))) |
106 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑁 − 1) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
108 | 105, 107 | preq12d 4220 |
. . . . . . . . 9
⊢ (𝑖 = (𝑁 − 1) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))}) |
109 | 108 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑖 = (𝑁 − 1) → ({((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸)) |
110 | 104, 109 | ralsn 4169 |
. . . . . . 7
⊢
(∀𝑖 ∈
{(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈ ran
𝐸) |
111 | 103, 110 | sylibr 223 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
112 | 88, 89, 89 | addsubd 10292 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = ((𝑁 − 1) +
1)) |
113 | 112 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
(0..^((𝑁 − 1) +
1))) |
114 | | nnm1nn0 11211 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
115 | | elnn0uz 11601 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈
(ℤ≥‘0)) |
116 | 114, 115 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
117 | | fzosplitsn 12442 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)})) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 − 1) + 1)) =
((0..^(𝑁 − 1)) ∪
{(𝑁 −
1)})) |
119 | 113, 118 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
((0..^(𝑁 − 1)) ∪
{(𝑁 −
1)})) |
120 | 119 | raleqdv 3121 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((𝑁 + 1) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
121 | | ralunb 3756 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
((0..^(𝑁 − 1)) ∪
{(𝑁 − 1)}){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
122 | 120, 121 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((𝑁 + 1) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
123 | 122 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
124 | 123 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
125 | 68, 111, 124 | mpbir2and 959 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
126 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 𝑃 ∈ Word 𝑉) |
127 | | ccatlen 13213 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((#‘𝑃) +
(#‘〈“(𝑃‘0)”〉))) |
128 | 126, 9, 127 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉))) |
129 | | id 22 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) = 𝑁 → (#‘𝑃) = 𝑁) |
130 | | s1len 13238 |
. . . . . . . . . . . . 13
⊢
(#‘〈“(𝑃‘0)”〉) = 1 |
131 | 130 | a1i 11 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) = 𝑁 →
(#‘〈“(𝑃‘0)”〉) =
1) |
132 | 129, 131 | oveq12d 6567 |
. . . . . . . . . . 11
⊢
((#‘𝑃) = 𝑁 → ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉)) =
(𝑁 + 1)) |
133 | 132 | ad2antll 761 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉)) = (𝑁 + 1)) |
134 | 128, 133 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)) |
135 | 134 | 3adant3 1074 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)) |
136 | 135 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1) =
((𝑁 + 1) −
1)) |
137 | 136 | oveq2d 6565 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1)) =
(0..^((𝑁 + 1) −
1))) |
138 | 137 | raleqdv 3121 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
139 | 125, 138 | mpbird 246 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) |
140 | 6, 12, 139 | 3jca 1235 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
141 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
142 | | iswwlkn 26212 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)))) |
143 | 141, 142 | syl3an3 1353 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)))) |
144 | | iswwlk 26211 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
145 | 144 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑉 WWalks 𝐸) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸))) |
146 | 145 | anbi1d 737 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑉 WWalks 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)) ↔ (((𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅ ∧ (𝑃 ++
〈“(𝑃‘0)”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)))) |
147 | 143, 146 | bitrd 267 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)))) |
148 | 147 | 3ad2ant1 1075 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ ran 𝐸) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)))) |
149 | 140, 135,
148 | mpbir2and 959 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
150 | | lswccats1 13263 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘0) ∈ 𝑉) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑃‘0)) |
151 | 1, 2, 150 | syl2anc 691 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑃‘0)) |
152 | | lbfzo0 12375 |
. . . . . . . . 9
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
153 | 152 | biimpri 217 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ∈
(0..^𝑁)) |
154 | 153 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^𝑁)) |
155 | 45 | eleq2d 2673 |
. . . . . . . 8
⊢
((#‘𝑃) = 𝑁 → (0 ∈
(0..^(#‘𝑃)) ↔ 0
∈ (0..^𝑁))) |
156 | 155 | ad2antll 761 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁))) |
157 | 154, 156 | mpbird 246 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^(#‘𝑃))) |
158 | | ccatval1 13214 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ 0 ∈
(0..^(#‘𝑃))) →
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
= (𝑃‘0)) |
159 | 1, 14, 157, 158 | syl3anc 1318 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0) = (𝑃‘0)) |
160 | 151, 159 | eqtr4d 2647 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
161 | 160 | 3ad2antl3 1218 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
162 | 161 | 3adant3 1074 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
163 | | fveq2 6103 |
. . . 4
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → ( lastS
‘𝑤) = ( lastS
‘(𝑃 ++
〈“(𝑃‘0)”〉))) |
164 | | fveq1 6102 |
. . . 4
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → (𝑤‘0) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
165 | 163, 164 | eqeq12d 2625 |
. . 3
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → (( lastS
‘𝑤) = (𝑤‘0) ↔ ( lastS
‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0))) |
166 | | clwwlkbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
167 | 165, 166 | elrab2 3333 |
. 2
⊢ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
𝐷 ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0))) |
168 | 149, 162,
167 | sylanbrc 695 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ 𝐷) |