Proof of Theorem wlklenvclwlk
Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) ↔ 〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉 ∈ (𝑉 Walks 𝐸)) |
2 | | wlkbprop 26051 |
. . . 4
⊢ (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) →
((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ (𝑊 ++ 〈“(𝑊‘0)”〉) ∈
V))) |
3 | | wlklenvp1 26365 |
. . . . . . 7
⊢ (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) →
(#‘(𝑊 ++
〈“(𝑊‘0)”〉)) = ((#‘𝐹) + 1)) |
4 | | wrdsymb1 13197 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (𝑊‘0) ∈ 𝑉) |
5 | 4 | s1cld 13236 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → 〈“(𝑊‘0)”〉 ∈ Word 𝑉) |
6 | | ccatlen 13213 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → (#‘(𝑊 ++ 〈“(𝑊‘0)”〉)) =
((#‘𝑊) +
(#‘〈“(𝑊‘0)”〉))) |
7 | 5, 6 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘(𝑊 ++ 〈“(𝑊‘0)”〉)) = ((#‘𝑊) + (#‘〈“(𝑊‘0)”〉))) |
8 | | s1len 13238 |
. . . . . . . . . . . . 13
⊢
(#‘〈“(𝑊‘0)”〉) = 1 |
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘〈“(𝑊‘0)”〉) =
1) |
10 | 9 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → ((#‘𝑊) + (#‘〈“(𝑊‘0)”〉)) = ((#‘𝑊) + 1)) |
11 | 7, 10 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘(𝑊 ++ 〈“(𝑊‘0)”〉)) = ((#‘𝑊) + 1)) |
12 | 11 | eqeq1d 2612 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → ((#‘(𝑊 ++ 〈“(𝑊‘0)”〉)) = ((#‘𝐹) + 1) ↔ ((#‘𝑊) + 1) = ((#‘𝐹) + 1))) |
13 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
14 | | eqcom 2617 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) + 1) =
((#‘𝐹) + 1) ↔
((#‘𝐹) + 1) =
((#‘𝑊) +
1)) |
15 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
16 | 15 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) →
(#‘𝐹) ∈
ℂ) |
17 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℂ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) →
(#‘𝑊) ∈
ℂ) |
19 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) → 1
∈ ℂ) |
20 | 16, 18, 19 | addcan2d 10119 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) →
(((#‘𝐹) + 1) =
((#‘𝑊) + 1) ↔
(#‘𝐹) =
(#‘𝑊))) |
21 | 20 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) →
(((#‘𝐹) + 1) =
((#‘𝑊) + 1) →
(#‘𝐹) =
(#‘𝑊))) |
22 | 14, 21 | syl5bi 231 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝐹) ∈ ℕ0) →
(((#‘𝑊) + 1) =
((#‘𝐹) + 1) →
(#‘𝐹) =
(#‘𝑊))) |
23 | 22 | ex 449 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝐹) ∈ ℕ0 →
(((#‘𝑊) + 1) =
((#‘𝐹) + 1) →
(#‘𝐹) =
(#‘𝑊)))) |
24 | 23 | com23 84 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ0 → (((#‘𝑊) + 1) = ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) =
(#‘𝑊)))) |
25 | 13, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (((#‘𝑊) + 1) = ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) =
(#‘𝑊)))) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (((#‘𝑊) + 1) = ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) =
(#‘𝑊)))) |
27 | 12, 26 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → ((#‘(𝑊 ++ 〈“(𝑊‘0)”〉)) = ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ0
→ (#‘𝐹) =
(#‘𝑊)))) |
28 | 27 | com3l 87 |
. . . . . . 7
⊢
((#‘(𝑊 ++
〈“(𝑊‘0)”〉)) = ((#‘𝐹) + 1) → ((#‘𝐹) ∈ ℕ0
→ ((𝑊 ∈ Word
𝑉 ∧ 1 ≤
(#‘𝑊)) →
(#‘𝐹) =
(#‘𝑊)))) |
29 | 3, 28 | syl 17 |
. . . . . 6
⊢ (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) →
((#‘𝐹) ∈
ℕ0 → ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘𝐹) = (#‘𝑊)))) |
30 | 29 | com12 32 |
. . . . 5
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) → ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘𝐹) = (#‘𝑊)))) |
31 | 30 | 3ad2ant1 1075 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ (𝑊 ++ 〈“(𝑊‘0)”〉) ∈ V)) →
(𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) → ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘𝐹) = (#‘𝑊)))) |
32 | 2, 31 | mpcom 37 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)(𝑊 ++ 〈“(𝑊‘0)”〉) → ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘𝐹) = (#‘𝑊))) |
33 | 1, 32 | sylbir 224 |
. 2
⊢
(〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉
∈ (𝑉 Walks 𝐸) → ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (#‘𝐹) = (#‘𝑊))) |
34 | 33 | com12 32 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉 ∈ (𝑉 Walks 𝐸) → (#‘𝐹) = (#‘𝑊))) |