Proof of Theorem wlklnwwlkln2lem
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | 1 | wwlknbp 29862 |
. . 3
⊢ (𝑃 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word (Vtx‘𝐺))) |
| 3 | | iswwlksn 29858 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑃 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1)))) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
(𝑃 ∈ (𝑁 WWalksN 𝐺) ↔ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1)))) |
| 5 | | lencl 14571 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (♯‘𝑃) ∈
ℕ0) |
| 6 | 5 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (♯‘𝑃) ∈
ℂ) |
| 7 | 6 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
(♯‘𝑃) ∈
ℂ) |
| 8 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) → 1
∈ ℂ) |
| 9 | | nn0cn 12536 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) → 𝑁 ∈
ℂ) |
| 11 | 7, 8, 10 | subadd2d 11639 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
(((♯‘𝑃) −
1) = 𝑁 ↔ (𝑁 + 1) = (♯‘𝑃))) |
| 12 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) = (♯‘𝑃) ↔ (♯‘𝑃) = (𝑁 + 1)) |
| 13 | 11, 12 | bitr2di 288 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
((♯‘𝑃) = (𝑁 + 1) ↔
((♯‘𝑃) −
1) = 𝑁)) |
| 14 | 13 | biimpcd 249 |
. . . . . . . . 9
⊢
((♯‘𝑃) =
(𝑁 + 1) → ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
((♯‘𝑃) −
1) = 𝑁)) |
| 15 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word (Vtx‘𝐺)) → ((♯‘𝑃) − 1) = 𝑁)) |
| 16 | 15 | impcom 407 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) → ((♯‘𝑃) − 1) = 𝑁) |
| 17 | | wlklnwwlkln2lem.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
| 18 | 17 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (WWalks‘𝐺) → (𝜑 → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1)) → (𝜑 → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) → (𝜑 → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) |
| 21 | 20 | imp 406 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) → ∃𝑓 𝑓(Walks‘𝐺)𝑃) |
| 22 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word (Vtx‘𝐺))
∧ (𝑃 ∈
(WWalks‘𝐺) ∧
(♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) ∧ 𝑓(Walks‘𝐺)𝑃) → 𝑓(Walks‘𝐺)𝑃) |
| 23 | | wlklenvm1 29640 |
. . . . . . . . . . . . 13
⊢ (𝑓(Walks‘𝐺)𝑃 → (♯‘𝑓) = ((♯‘𝑃) − 1)) |
| 24 | 22, 23 | jccir 521 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word (Vtx‘𝐺))
∧ (𝑃 ∈
(WWalks‘𝐺) ∧
(♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) ∧ 𝑓(Walks‘𝐺)𝑃) → (𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1))) |
| 25 | 24 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) → (𝑓(Walks‘𝐺)𝑃 → (𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1)))) |
| 26 | 25 | eximdv 1917 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) → (∃𝑓 𝑓(Walks‘𝐺)𝑃 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1)))) |
| 27 | 21, 26 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1))) |
| 28 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢
(((♯‘𝑃)
− 1) = 𝑁 →
((♯‘𝑓) =
((♯‘𝑃) −
1) ↔ (♯‘𝑓)
= 𝑁)) |
| 29 | 28 | anbi2d 630 |
. . . . . . . . . 10
⊢
(((♯‘𝑃)
− 1) = 𝑁 →
((𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1)) ↔ (𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |
| 30 | 29 | exbidv 1921 |
. . . . . . . . 9
⊢
(((♯‘𝑃)
− 1) = 𝑁 →
(∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = ((♯‘𝑃) − 1)) ↔ ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |
| 31 | 27, 30 | imbitrid 244 |
. . . . . . . 8
⊢
(((♯‘𝑃)
− 1) = 𝑁 →
((((𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word (Vtx‘𝐺))
∧ (𝑃 ∈
(WWalks‘𝐺) ∧
(♯‘𝑃) = (𝑁 + 1))) ∧ 𝜑) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |
| 32 | 31 | expd 415 |
. . . . . . 7
⊢
(((♯‘𝑃)
− 1) = 𝑁 →
(((𝑁 ∈
ℕ0 ∧ 𝑃
∈ Word (Vtx‘𝐺))
∧ (𝑃 ∈
(WWalks‘𝐺) ∧
(♯‘𝑃) = (𝑁 + 1))) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))) |
| 33 | 16, 32 | mpcom 38 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) ∧ (𝑃 ∈ (WWalks‘𝐺) ∧ (♯‘𝑃) = (𝑁 + 1))) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |
| 34 | 33 | ex 412 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
((𝑃 ∈
(WWalks‘𝐺) ∧
(♯‘𝑃) = (𝑁 + 1)) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))) |
| 35 | 4, 34 | sylbid 240 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
(𝑃 ∈ (𝑁 WWalksN 𝐺) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))) |
| 36 | 35 | 3adant1 1131 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑃 ∈ Word
(Vtx‘𝐺)) →
(𝑃 ∈ (𝑁 WWalksN 𝐺) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁)))) |
| 37 | 2, 36 | mpcom 38 |
. 2
⊢ (𝑃 ∈ (𝑁 WWalksN 𝐺) → (𝜑 → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |
| 38 | 37 | com12 32 |
1
⊢ (𝜑 → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) |