Step | Hyp | Ref
| Expression |
1 | | wlkn0 27708 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) |
2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | upgriswlk 27728 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
5 | | simpr 488 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ≠ ∅) |
6 | | ffz0iswrd 14096 |
. . . . . . . 8
⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → 𝑃 ∈ Word (Vtx‘𝐺)) |
7 | 6 | 3ad2ant2 1136 |
. . . . . . 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 27193 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
10 | 3 | uhgrfun 27157 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
11 | | funfn 6410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
12 | 11 | biimpi 219 |
. . . . . . . . . . . . . . . . . 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 14082 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑖 ∈
(0..^(♯‘𝐹)))
→ (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
16 | 15 | ad4ant14 752 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
17 | | fnfvelrn 6901 |
. . . . . . . . . . . . . . . 16
⊢
(((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) ∧
(𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
18 | 14, 16, 17 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
19 | | edgval 27140 |
. . . . . . . . . . . . . . 15
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
20 | 18, 19 | eleqtrrdi 2849 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺)) |
21 | | eleq1 2825 |
. . . . . . . . . . . . . . 15
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑖)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
22 | 21 | eqcoms 2745 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
23 | 20, 22 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → (((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | 23 | ralimdva 3100 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph) → (∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
25 | 24 | ex 416 |
. . . . . . . . . . 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 1119 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐺 ∈ UPGraph → ∀𝑖 ∈
(0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
28 | 27 | impcom 411 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
29 | | lencl 14088 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(♯‘𝐹) ∈
ℕ0) |
30 | | ffz0hash 14011 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (♯‘𝑃) = ((♯‘𝐹) + 1)) |
31 | 30 | ex 416 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐹)
∈ ℕ0 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (♯‘𝑃) = ((♯‘𝐹) + 1))) |
32 | | oveq1 7220 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑃) =
((♯‘𝐹) + 1)
→ ((♯‘𝑃)
− 1) = (((♯‘𝐹) + 1) − 1)) |
33 | | nn0cn 12100 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
34 | | pncan1 11256 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐹)
∈ ℂ → (((♯‘𝐹) + 1) − 1) = (♯‘𝐹)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐹)
∈ ℕ0 → (((♯‘𝐹) + 1) − 1) = (♯‘𝐹)) |
36 | 32, 35 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ (♯‘𝑃) = ((♯‘𝐹) + 1)) → ((♯‘𝑃) − 1) =
(♯‘𝐹)) |
37 | 36 | ex 416 |
. . . . . . . . . . . . . . 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 410 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → ((♯‘𝑃) − 1) =
(♯‘𝐹)) |
41 | 40 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) →
(0..^((♯‘𝑃)
− 1)) = (0..^(♯‘𝐹))) |
42 | 41 | raleqdv 3325 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
43 | 42 | 3adant3 1134 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
44 | 43 | adantl 485 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
45 | 28, 44 | mpbird 260 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
46 | 45 | adantr 484 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → ∀𝑖 ∈
(0..^((♯‘𝑃)
− 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
47 | | eqid 2737 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
48 | 2, 47 | iswwlks 27920 |
. . . . . 6
⊢ (𝑃 ∈ (WWalks‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
49 | 5, 8, 46, 48 | syl3anbrc 1345 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ (WWalks‘𝐺)) |
50 | 49 | ex 416 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺))) |
51 | 50 | ex 416 |
. . 3
⊢ (𝐺 ∈ UPGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^(♯‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
52 | 4, 51 | sylbid 243 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
53 | 1, 52 | mpdi 45 |
1
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalks‘𝐺))) |