| Step | Hyp | Ref
| Expression |
| 1 | | wlkn0 29639 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 4 | 2, 3 | upgriswlk 29659 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
| 5 | | simpr 484 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ≠ ∅) |
| 6 | | ffz0iswrd 14579 |
. . . . . . . 8
⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → 𝑃 ∈ Word (Vtx‘𝐺)) |
| 7 | 6 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑃 ∈ Word (Vtx‘𝐺)) |
| 8 | 7 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ Word (Vtx‘𝐺)) |
| 9 | | upgruhgr 29119 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
| 10 | 3 | uhgrfun 29083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
| 11 | | funfn 6596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
| 12 | 11 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
(iEdg‘𝐺) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
| 13 | 9, 10, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
| 14 | 13 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
| 15 | | wrdsymbcl 14565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑖 ∈
(0..^(♯‘𝐹)))
→ (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
| 16 | 15 | ad4ant14 752 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
| 17 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . 16
⊢
(((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) ∧
(𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
| 18 | 14, 16, 17 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
| 19 | | edgval 29066 |
. . . . . . . . . . . . . . 15
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
| 20 | 18, 19 | eleqtrrdi 2852 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺)) |
| 21 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑖)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
| 22 | 21 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
| 23 | 20, 22 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → (((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 24 | 23 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 25 | 24 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (𝐺 ∈ UPGraph → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
| 26 | 25 | com23 86 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝐺 ∈ UPGraph → ∀𝑖 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
| 27 | 26 | 3impia 1118 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐺 ∈ UPGraph → ∀𝑖 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 28 | 27 | impcom 407 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 29 | | lencl 14571 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(♯‘𝐹) ∈
ℕ0) |
| 30 | | ffz0hash 14486 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (♯‘𝑃) = ((♯‘𝐹) + 1)) |
| 31 | 30 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹)
∈ ℕ0 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (♯‘𝑃) = ((♯‘𝐹) + 1))) |
| 32 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ ((♯‘𝑃)
− 1) = (((♯‘𝐹) + 1) − 1)) |
| 33 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
| 34 | | pncan1 11687 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℂ → (((♯‘𝐹) + 1) − 1) = (♯‘𝐹)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐹)
∈ ℕ0 → (((♯‘𝐹) + 1) − 1) = (♯‘𝐹)) |
| 36 | 32, 35 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ (♯‘𝑃) = ((♯‘𝐹) + 1)) → ((♯‘𝑃) − 1) =
(♯‘𝐹)) |
| 37 | 36 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹)
∈ ℕ0 → ((♯‘𝑃) = ((♯‘𝐹) + 1) → ((♯‘𝑃) − 1) =
(♯‘𝐹))) |
| 38 | 31, 37 | syld 47 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐹)
∈ ℕ0 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → ((♯‘𝑃) − 1) = (♯‘𝐹))) |
| 39 | 29, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → ((♯‘𝑃) − 1) = (♯‘𝐹))) |
| 40 | 39 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → ((♯‘𝑃) − 1) =
(♯‘𝐹)) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) →
(0..^((♯‘𝑃)
− 1)) = (0..^(♯‘𝐹))) |
| 42 | 41 | raleqdv 3326 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 43 | 42 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 44 | 43 | adantl 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 45 | 28, 44 | mpbird 257 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 46 | 45 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 47 | | eqid 2737 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 48 | 2, 47 | iswwlks 29856 |
. . . . . 6
⊢ (𝑃 ∈ (WWalks‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 49 | 5, 8, 46, 48 | syl3anbrc 1344 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ (WWalks‘𝐺)) |
| 50 | 49 | ex 412 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺))) |
| 51 | 50 | ex 412 |
. . 3
⊢ (𝐺 ∈ UPGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
| 52 | 4, 51 | sylbid 240 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
| 53 | 1, 52 | mpdi 45 |
1
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalks‘𝐺))) |