Proof of Theorem wlklenvclwlkOLD
Step | Hyp | Ref
| Expression |
1 | | df-br 5031 |
. . 3
⊢ (𝐹(Walks‘𝐺)(𝑊 ++ 〈“(𝑊‘0)”〉) ↔ 〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉 ∈
(Walks‘𝐺)) |
2 | | wlklenvp1 27560 |
. . . 4
⊢ (𝐹(Walks‘𝐺)(𝑊 ++ 〈“(𝑊‘0)”〉) →
(♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝐹) +
1)) |
3 | | wlkcl 27557 |
. . . 4
⊢ (𝐹(Walks‘𝐺)(𝑊 ++ 〈“(𝑊‘0)”〉) →
(♯‘𝐹) ∈
ℕ0) |
4 | | wrdsymb1 13994 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(𝑊‘0) ∈
(Vtx‘𝐺)) |
5 | 4 | s1cld 14046 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
〈“(𝑊‘0)”〉 ∈ Word
(Vtx‘𝐺)) |
6 | | ccatlenOLD 14017 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 〈“(𝑊‘0)”〉 ∈
Word (Vtx‘𝐺)) →
(♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉))) |
7 | 5, 6 | syldan 594 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉))) |
8 | | s1len 14049 |
. . . . . . . . . 10
⊢
(♯‘〈“(𝑊‘0)”〉) = 1 |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(♯‘〈“(𝑊‘0)”〉) =
1) |
10 | 9 | oveq2d 7186 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
1)) |
11 | 7, 10 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
1)) |
12 | 11 | eqeq1d 2740 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝐹) + 1)
↔ ((♯‘𝑊) +
1) = ((♯‘𝐹) +
1))) |
13 | | lencl 13974 |
. . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘𝑊) ∈
ℕ0) |
14 | | eqcom 2745 |
. . . . . . . . . . 11
⊢
(((♯‘𝑊)
+ 1) = ((♯‘𝐹) +
1) ↔ ((♯‘𝐹) + 1) = ((♯‘𝑊) + 1)) |
15 | | nn0cn 11986 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
16 | 15 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) →
(♯‘𝐹) ∈
ℂ) |
17 | | nn0cn 11986 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ ℂ) |
18 | 17 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) →
(♯‘𝑊) ∈
ℂ) |
19 | | 1cnd 10714 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) → 1
∈ ℂ) |
20 | 16, 18, 19 | addcan2d 10922 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) →
(((♯‘𝐹) + 1) =
((♯‘𝑊) + 1)
↔ (♯‘𝐹) =
(♯‘𝑊))) |
21 | 20 | biimpd 232 |
. . . . . . . . . . 11
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) →
(((♯‘𝐹) + 1) =
((♯‘𝑊) + 1)
→ (♯‘𝐹) =
(♯‘𝑊))) |
22 | 14, 21 | syl5bi 245 |
. . . . . . . . . 10
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) →
(((♯‘𝑊) + 1) =
((♯‘𝐹) + 1)
→ (♯‘𝐹) =
(♯‘𝑊))) |
23 | 22 | ex 416 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝐹) ∈ ℕ0 →
(((♯‘𝑊) + 1) =
((♯‘𝐹) + 1)
→ (♯‘𝐹) =
(♯‘𝑊)))) |
24 | 23 | com23 86 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 → (((♯‘𝑊) + 1) = ((♯‘𝐹) + 1) → ((♯‘𝐹) ∈ ℕ0
→ (♯‘𝐹) =
(♯‘𝑊)))) |
25 | 13, 24 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (((♯‘𝑊) + 1) = ((♯‘𝐹) + 1) →
((♯‘𝐹) ∈
ℕ0 → (♯‘𝐹) = (♯‘𝑊)))) |
26 | 25 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(((♯‘𝑊) + 1) =
((♯‘𝐹) + 1)
→ ((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) = (♯‘𝑊)))) |
27 | 12, 26 | sylbid 243 |
. . . . 5
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) =
((♯‘𝐹) + 1)
→ ((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) = (♯‘𝑊)))) |
28 | 27 | com3l 89 |
. . . 4
⊢
((♯‘(𝑊
++ 〈“(𝑊‘0)”〉)) =
((♯‘𝐹) + 1)
→ ((♯‘𝐹)
∈ ℕ0 → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (♯‘𝑊)) → (♯‘𝐹) = (♯‘𝑊)))) |
29 | 2, 3, 28 | sylc 65 |
. . 3
⊢ (𝐹(Walks‘𝐺)(𝑊 ++ 〈“(𝑊‘0)”〉) → ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(♯‘𝐹) =
(♯‘𝑊))) |
30 | 1, 29 | sylbir 238 |
. 2
⊢
(〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉
∈ (Walks‘𝐺)
→ ((𝑊 ∈ Word
(Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(♯‘𝐹) =
(♯‘𝑊))) |
31 | 30 | com12 32 |
1
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤
(♯‘𝑊)) →
(〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉
∈ (Walks‘𝐺)
→ (♯‘𝐹) =
(♯‘𝑊))) |