Proof of Theorem clwwlksel
Step | Hyp | Ref
| Expression |
1 | | simprl 794 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 𝑃 ∈ Word (Vtx‘𝐺)) |
2 | | fstwrdne0 13345 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) ∈ (Vtx‘𝐺)) |
3 | | ccatws1n0 13409 |
. . . . . 6
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
5 | 4 | 3adant3 1081 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅) |
6 | | simp2l 1087 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → 𝑃 ∈ Word (Vtx‘𝐺)) |
7 | 2 | s1cld 13383 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 〈“(𝑃‘0)”〉 ∈ Word
(Vtx‘𝐺)) |
8 | 7 | 3adant3 1081 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺)) |
9 | | ccatcl 13359 |
. . . . 5
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺)) →
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word (Vtx‘𝐺)) |
10 | 6, 8, 9 | syl2anc 693 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word
(Vtx‘𝐺)) |
11 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑃 ∈ Word (Vtx‘𝐺)) |
12 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺)) |
13 | | elfzonn0 12512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) → 𝑖 ∈ ℕ0) |
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ ℕ0) |
15 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑁 ∈ ℤ) |
17 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ ∧
𝑖 < (𝑁 − 1))) |
18 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑖 ∈
ℝ) |
20 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
21 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 1) ∈
ℝ) |
24 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℝ) |
25 | 19, 23, 24 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑖 ∈ ℝ
∧ (𝑁 − 1) ∈
ℝ ∧ 𝑁 ∈
ℝ)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → (𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈
ℝ)) |
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → 𝑖 < (𝑁 − 1)) |
28 | 20 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑁 − 1) <
𝑁) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → (𝑁 − 1) < 𝑁) |
31 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ) →
((𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁) → 𝑖 < 𝑁)) |
32 | 31 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ) ∧
(𝑖 < (𝑁 − 1) ∧ (𝑁 − 1) < 𝑁)) → 𝑖 < 𝑁) |
33 | 26, 27, 30, 32 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
∧ 𝑖 < (𝑁 − 1)) → 𝑖 < 𝑁) |
34 | 33 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑖 < (𝑁 − 1) → 𝑖 < 𝑁)) |
35 | 34 | impancom 456 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℕ0
∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
36 | 35 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ ℕ0
∧ (𝑁 − 1) ∈
ℕ ∧ 𝑖 < (𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
37 | 17, 36 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0..^(𝑁 − 1)) → (𝑁 ∈ ℕ → 𝑖 < 𝑁)) |
38 | 37 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 < 𝑁) |
39 | | elfzo0z 12509 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁)) |
40 | 14, 16, 38, 39 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
41 | 40 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^𝑁)) |
42 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) = 𝑁 → (0..^(#‘𝑃)) = (0..^𝑁)) |
43 | 42 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) = 𝑁 → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
44 | 43 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 ∈ (0..^(#‘𝑃)) ↔ 𝑖 ∈ (0..^𝑁))) |
46 | 41, 45 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → 𝑖 ∈ (0..^(#‘𝑃))) |
47 | | ccatval1 13361 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
𝑖 ∈
(0..^(#‘𝑃))) →
((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = (𝑃‘𝑖)) |
48 | 11, 12, 46, 47 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = (𝑃‘𝑖)) |
49 | 48 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘𝑖) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖)) |
50 | | elfzom1p1elfzo 12547 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
51 | 50 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^𝑁)) |
52 | 42 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0..^(#‘𝑃)) = (0..^𝑁)) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (0..^(#‘𝑃)) = (0..^𝑁)) |
54 | 51, 53 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝑃))) |
55 | | ccatval1 13361 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
(𝑖 + 1) ∈
(0..^(#‘𝑃))) →
((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
56 | 11, 12, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
57 | 56 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))) |
58 | 49, 57 | preq12d 4276 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))}) |
59 | 58 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) ∧ 𝑖 ∈ (0..^(𝑁 − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
60 | 59 | ralbidva 2985 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
61 | 60 | biimpcd 239 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
62 | 61 | adantr 481 |
. . . . . . . 8
⊢
((∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
63 | 62 | expdcom 455 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
64 | 63 | 3imp 1256 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
65 | | fzo0end 12560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁)) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^𝑁)) |
67 | 42 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑃) = 𝑁 → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁))) |
68 | 67 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑁 − 1) ∈ (0..^(#‘𝑃)) ↔ (𝑁 − 1) ∈ (0..^𝑁))) |
69 | 66, 68 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑁 − 1) ∈ (0..^(#‘𝑃))) |
70 | | ccatval1 13361 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺) ∧
(𝑁 − 1) ∈
(0..^(#‘𝑃))) →
((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1))) |
71 | 1, 7, 69, 70 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)) = (𝑃‘(𝑁 − 1))) |
72 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑃) → (𝑁 − 1) = ((#‘𝑃) − 1)) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑃) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
74 | 73 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑃) = 𝑁 → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
75 | 74 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = (𝑃‘((#‘𝑃) − 1))) |
76 | | lsw 13351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
78 | 75, 77 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃)) |
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘(𝑁 − 1)) = ( lastS ‘𝑃)) |
80 | 71, 79 | eqtr2d 2657 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘𝑃) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1))) |
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = (#‘𝑃) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
82 | 81 | eqcoms 2630 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑃) = 𝑁 → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
83 | 82 | ad2antll 765 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃))) |
84 | | nncn 11028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
85 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
86 | 84, 85 | npcand 10396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
87 | 86 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 = ((𝑁 − 1) + 1)) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
89 | 88 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑁) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
90 | | ccatws1ls 13410 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃)) = (𝑃‘0)) |
91 | 1, 2, 90 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(#‘𝑃)) = (𝑃‘0)) |
92 | 83, 89, 91 | 3eqtr3rd 2665 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (𝑃‘0) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
93 | 80, 92 | preq12d 4276 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {( lastS ‘𝑃), (𝑃‘0)} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))}) |
94 | 93 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺))) |
95 | 94 | biimpcd 239 |
. . . . . . . . . 10
⊢ ({( lastS
‘𝑃), (𝑃‘0)} ∈
(Edg‘𝐺) →
((𝑁 ∈ ℕ ∧
(𝑃 ∈ Word
(Vtx‘𝐺) ∧
(#‘𝑃) = 𝑁)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺))) |
96 | 95 | adantl 482 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺))) |
97 | 96 | expdcom 455 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) → ((∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺)) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺)))) |
98 | 97 | 3imp 1256 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺)) |
99 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑁 − 1) ∈
V |
100 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑁 − 1) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1))) |
101 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
102 | 101 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑁 − 1) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))) |
103 | 100, 102 | preq12d 4276 |
. . . . . . . . 9
⊢ (𝑖 = (𝑁 − 1) → {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} = {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) +
1))}) |
104 | 103 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑖 = (𝑁 − 1) → ({((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺))) |
105 | 99, 104 | ralsn 4222 |
. . . . . . 7
⊢
(∀𝑖 ∈
{(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑁 − 1)), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘((𝑁 − 1) + 1))} ∈
(Edg‘𝐺)) |
106 | 98, 105 | sylibr 224 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
107 | 84, 85, 85 | addsubd 10413 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = ((𝑁 − 1) +
1)) |
108 | 107 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
(0..^((𝑁 − 1) +
1))) |
109 | | nnm1nn0 11334 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
110 | | elnn0uz 11725 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈
(ℤ≥‘0)) |
111 | 109, 110 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
112 | | fzosplitsn 12576 |
. . . . . . . . . . 11
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → (0..^((𝑁 − 1) + 1)) = ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)})) |
113 | 111, 112 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 − 1) + 1)) =
((0..^(𝑁 − 1)) ∪
{(𝑁 −
1)})) |
114 | 108, 113 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(0..^((𝑁 + 1) − 1)) =
((0..^(𝑁 − 1)) ∪
{(𝑁 −
1)})) |
115 | 114 | raleqdv 3144 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((𝑁 + 1) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^(𝑁 − 1)) ∪ {(𝑁 − 1)}){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
116 | | ralunb 3794 |
. . . . . . . 8
⊢
(∀𝑖 ∈
((0..^(𝑁 − 1)) ∪
{(𝑁 − 1)}){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
117 | 115, 116 | syl6bb 276 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(∀𝑖 ∈
(0..^((𝑁 + 1) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^(𝑁 − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {(𝑁 − 1)} {((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
118 | 117 | 3ad2ant1 1082 |
. . . . . 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‘𝐺)))) |
119 | 64, 106, 118 | mpbir2and 957 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
120 | | ccatlen 13360 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺)) →
(#‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉))) |
121 | 1, 7, 120 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉))) |
122 | | id 22 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) = 𝑁 → (#‘𝑃) = 𝑁) |
123 | | s1len 13385 |
. . . . . . . . . . . . 13
⊢
(#‘〈“(𝑃‘0)”〉) = 1 |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) = 𝑁 →
(#‘〈“(𝑃‘0)”〉) =
1) |
125 | 122, 124 | oveq12d 6668 |
. . . . . . . . . . 11
⊢
((#‘𝑃) = 𝑁 → ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉)) =
(𝑁 + 1)) |
126 | 125 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((#‘𝑃) + (#‘〈“(𝑃‘0)”〉)) = (𝑁 + 1)) |
127 | 121, 126 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑁 + 1)) |
128 | 127 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)) |
129 | 128 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1) = ((𝑁 + 1) −
1)) |
130 | 129 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)) = (0..^((𝑁 + 1) −
1))) |
131 | 130 | raleqdv 3144 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
132 | 119, 131 | mpbird 247 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ∀𝑖 ∈ (0..^((#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1)){((𝑃 ++
〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
133 | 5, 10, 132 | 3jca 1242 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word (Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
134 | | nnnn0 11299 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
135 | | iswwlksn 26730 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((𝑃 ++
〈“(𝑃‘0)”〉) ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(WWalks‘𝐺) ∧
(#‘(𝑃 ++
〈“(𝑃‘0)”〉)) = (𝑁 + 1)))) |
136 | 134, 135 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(𝑁 WWalksN 𝐺) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(WWalks‘𝐺) ∧
(#‘(𝑃 ++
〈“(𝑃‘0)”〉)) = (𝑁 + 1)))) |
137 | | eqid 2622 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
138 | | eqid 2622 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
139 | 137, 138 | iswwlks 26728 |
. . . . . . 7
⊢ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(WWalks‘𝐺) ↔
((𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅ ∧ (𝑃 ++
〈“(𝑃‘0)”〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
140 | 139 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(WWalks‘𝐺) ↔
((𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅ ∧ (𝑃 ++
〈“(𝑃‘0)”〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
141 | 140 | anbi1d 741 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(WWalks‘𝐺) ∧
(#‘(𝑃 ++
〈“(𝑃‘0)”〉)) = (𝑁 + 1)) ↔ (((𝑃 ++ 〈“(𝑃‘0)”〉) ≠
∅ ∧ (𝑃 ++
〈“(𝑃‘0)”〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)))) |
142 | 136, 141 | bitrd 268 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(𝑁 WWalksN 𝐺) ↔ (((𝑃 ++ 〈“(𝑃‘0)”〉) ≠ ∅ ∧
(𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word (Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)){((𝑃 ++ 〈“(𝑃‘0)”〉)‘𝑖), ((𝑃 ++ 〈“(𝑃‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (#‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑁 + 1)))) |
143 | 142 | 3ad2ant1 1082 |
. . 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)))) |
144 | 133, 128,
143 | mpbir2and 957 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ (𝑁 WWalksN 𝐺)) |
145 | | lswccats1 13411 |
. . . . 5
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑃‘0) ∈ (Vtx‘𝐺)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
(𝑃‘0)) |
146 | 1, 2, 145 | syl2anc 693 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = (𝑃‘0)) |
147 | | lbfzo0 12507 |
. . . . . . . 8
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
148 | 147 | biimpri 218 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ∈
(0..^𝑁)) |
149 | 148 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^𝑁)) |
150 | 42 | eleq2d 2687 |
. . . . . . 7
⊢
((#‘𝑃) = 𝑁 → (0 ∈
(0..^(#‘𝑃)) ↔ 0
∈ (0..^𝑁))) |
151 | 150 | ad2antll 765 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → (0 ∈ (0..^(#‘𝑃)) ↔ 0 ∈ (0..^𝑁))) |
152 | 149, 151 | mpbird 247 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → 0 ∈ (0..^(#‘𝑃))) |
153 | | ccatval1 13361 |
. . . . 5
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑃‘0)”〉 ∈
Word (Vtx‘𝐺) ∧ 0
∈ (0..^(#‘𝑃)))
→ ((𝑃 ++
〈“(𝑃‘0)”〉)‘0) = (𝑃‘0)) |
154 | 1, 7, 152, 153 | syl3anc 1326 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0) = (𝑃‘0)) |
155 | 146, 154 | eqtr4d 2659 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁)) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
156 | 155 | 3adant3 1081 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
157 | | fveq2 6191 |
. . . 4
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → ( lastS
‘𝑤) = ( lastS
‘(𝑃 ++
〈“(𝑃‘0)”〉))) |
158 | | fveq1 6190 |
. . . 4
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → (𝑤‘0) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
159 | 157, 158 | eqeq12d 2637 |
. . 3
⊢ (𝑤 = (𝑃 ++ 〈“(𝑃‘0)”〉) → (( lastS
‘𝑤) = (𝑤‘0) ↔ ( lastS
‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0))) |
160 | | clwwlksbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
161 | 159, 160 | elrab2 3366 |
. 2
⊢ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
𝐷 ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) ∈
(𝑁 WWalksN 𝐺) ∧ ( lastS ‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0))) |
162 | 144, 156,
161 | sylanbrc 698 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ 𝐷) |