Proof of Theorem wlklniswwlkn2
Step | Hyp | Ref
| Expression |
1 | | wwlknprop 26214 |
. . 3
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word 𝑉))) |
2 | | simpl 472 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝑉 ∈ V) |
3 | 2 | adantr 480 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → 𝑉 ∈ V) |
4 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
5 | 4 | adantr 480 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → 𝐸 ∈ V) |
6 | | simpl 472 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → 𝑁 ∈
ℕ0) |
7 | 6 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → 𝑁 ∈
ℕ0) |
8 | | iswwlkn 26212 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)))) |
9 | 3, 5, 7, 8 | syl3anc 1318 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)))) |
10 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
11 | 10 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℂ) |
12 | 11 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → (#‘𝑃) ∈
ℂ) |
13 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → 1 ∈
ℂ) |
14 | | nn0cn 11179 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → 𝑁 ∈ ℂ) |
16 | 12, 13, 15 | subadd2d 10290 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → (((#‘𝑃) − 1) = 𝑁 ↔ (𝑁 + 1) = (#‘𝑃))) |
17 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) = (#‘𝑃) ↔ (#‘𝑃) = (𝑁 + 1)) |
18 | 16, 17 | syl6rbb 276 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉) → ((#‘𝑃) = (𝑁 + 1) ↔ ((#‘𝑃) − 1) = 𝑁)) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → ((#‘𝑃) = (𝑁 + 1) ↔ ((#‘𝑃) − 1) = 𝑁)) |
20 | 19 | biimpcd 238 |
. . . . . . . 8
⊢
((#‘𝑃) =
(𝑁 + 1) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → ((#‘𝑃) − 1) = 𝑁)) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ ((𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word 𝑉)) → ((#‘𝑃) − 1) = 𝑁)) |
22 | 21 | impcom 445 |
. . . . . 6
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) ∧ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) → ((#‘𝑃) − 1) = 𝑁) |
23 | | wlkiswwlk2 26225 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 WWalks 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
24 | 23 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
25 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
26 | 25 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) ∧ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) → (𝑉 USGrph 𝐸 → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) |
27 | 26 | imp 444 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃) |
28 | | simpr 476 |
. . . . . . . . . . . 12
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) ∧ 𝑓(𝑉 Walks 𝐸)𝑃) → 𝑓(𝑉 Walks 𝐸)𝑃) |
29 | | wlklenvm1 26060 |
. . . . . . . . . . . 12
⊢ (𝑓(𝑉 Walks 𝐸)𝑃 → (#‘𝑓) = ((#‘𝑃) − 1)) |
30 | 28, 29 | jccir 560 |
. . . . . . . . . . 11
⊢
((((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) ∧ 𝑓(𝑉 Walks 𝐸)𝑃) → (𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1))) |
31 | 30 | ex 449 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) → (𝑓(𝑉 Walks 𝐸)𝑃 → (𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1)))) |
32 | 31 | eximdv 1833 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) → (∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1)))) |
33 | 27, 32 | mpd 15 |
. . . . . . . 8
⊢
(((((𝑉 ∈ V
∧ 𝐸 ∈ V) ∧
(𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word 𝑉)) ∧
(𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1))) |
34 | | eqeq2 2621 |
. . . . . . . . . 10
⊢
(((#‘𝑃)
− 1) = 𝑁 →
((#‘𝑓) =
((#‘𝑃) − 1)
↔ (#‘𝑓) = 𝑁)) |
35 | 34 | anbi2d 736 |
. . . . . . . . 9
⊢
(((#‘𝑃)
− 1) = 𝑁 →
((𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1)) ↔ (𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |
36 | 35 | exbidv 1837 |
. . . . . . . 8
⊢
(((#‘𝑃)
− 1) = 𝑁 →
(∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = ((#‘𝑃) − 1)) ↔ ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |
37 | 33, 36 | syl5ib 233 |
. . . . . . 7
⊢
(((#‘𝑃)
− 1) = 𝑁 →
(((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) ∧ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) ∧ 𝑉 USGrph 𝐸) → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |
38 | 37 | expd 451 |
. . . . . 6
⊢
(((#‘𝑃)
− 1) = 𝑁 →
((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) ∧ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁)))) |
39 | 22, 38 | mpcom 37 |
. . . . 5
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) ∧ (𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1))) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |
40 | 39 | ex 449 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → ((𝑃 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑃) = (𝑁 + 1)) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁)))) |
41 | 9, 40 | sylbid 229 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word 𝑉)) → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁)))) |
42 | 1, 41 | mpcom 37 |
. 2
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑉 USGrph 𝐸 → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |
43 | 42 | com12 32 |
1
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) |