Step | Hyp | Ref
| Expression |
1 | | wlkn0 26516 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) |
2 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
4 | 2, 3 | upgriswlk 26537 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
5 | | simpr 477 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ≠ ∅) |
6 | | ffz0iswrd 13332 |
. . . . . . . 8
⊢ (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → 𝑃 ∈ Word (Vtx‘𝐺)) |
7 | 6 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑃 ∈ Word (Vtx‘𝐺)) |
8 | 7 | ad2antlr 763 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ Word (Vtx‘𝐺)) |
9 | | upgruhgr 25997 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph
) |
10 | 3 | uhgrfun 25961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
11 | | funfn 5918 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
12 | 11 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
(iEdg‘𝐺) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
13 | 9, 10, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
14 | 13 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
15 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
16 | 15 | ad4ant14 1293 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) |
17 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . 16
⊢
(((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) ∧
(𝐹‘𝑖) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
18 | 14, 16, 17 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ ran (iEdg‘𝐺)) |
19 | | edgval 25941 |
. . . . . . . . . . . . . . 15
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
20 | 18, 19 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺)) |
21 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = ((iEdg‘𝐺)‘(𝐹‘𝑖)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
22 | 21 | eqcoms 2630 |
. . . . . . . . . . . . . 14
⊢
(((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ((iEdg‘𝐺)‘(𝐹‘𝑖)) ∈ (Edg‘𝐺))) |
23 | 20, 22 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ (0..^(#‘𝐹))) → (((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | 23 | ralimdva 2962 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) ∧ 𝐺 ∈ UPGraph ) → (∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
25 | 24 | ex 450 |
. . . . . . . . . . 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 1261 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝐺 ∈ UPGraph → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
28 | 27 | impcom 446 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
29 | | lencl 13324 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(#‘𝐹) ∈
ℕ0) |
30 | | ffz0hash 13231 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (#‘𝑃) = ((#‘𝐹) + 1)) |
31 | 30 | ex 450 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) ∈
ℕ0 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) → (#‘𝑃) = ((#‘𝐹) + 1))) |
32 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
((#‘𝑃) − 1) =
(((#‘𝐹) + 1) −
1)) |
33 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
34 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℂ → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) ∈
ℕ0 → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
36 | 32, 35 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘𝑃) = ((#‘𝐹) + 1)) → ((#‘𝑃) − 1) = (#‘𝐹)) |
37 | 36 | ex 450 |
. . . . . . . . . . . . . . 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 445 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → ((#‘𝑃) − 1) = (#‘𝐹)) |
41 | 40 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (0..^((#‘𝑃) − 1)) = (0..^(#‘𝐹))) |
42 | 41 | raleqdv 3144 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
43 | 42 | 3adant3 1081 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
44 | 43 | adantl 482 |
. . . . . . . 8
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(#‘𝐹)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
45 | 28, 44 | mpbird 247 |
. . . . . . 7
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
46 | 45 | adantr 481 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
47 | | eqid 2622 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
48 | 2, 47 | iswwlks 26728 |
. . . . . 6
⊢ (𝑃 ∈ (WWalks‘𝐺) ↔ (𝑃 ≠ ∅ ∧ 𝑃 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
49 | 5, 8, 46, 48 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) ∧ 𝑃 ≠ ∅) → 𝑃 ∈ (WWalks‘𝐺)) |
50 | 49 | ex 450 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺))) |
51 | 50 | ex 450 |
. . 3
⊢ (𝐺 ∈ UPGraph → ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^(#‘𝐹))((iEdg‘𝐺)‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
52 | 4, 51 | sylbid 230 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → (𝑃 ≠ ∅ → 𝑃 ∈ (WWalks‘𝐺)))) |
53 | 1, 52 | mpdi 45 |
1
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalks‘𝐺))) |