Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | eqid 2733 |
. . 3
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
3 | 1, 2 | upwlkbprop 46126 |
. 2
β’ (πΉ(UPWalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) |
4 | | idd 24 |
. . . 4
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ β Word dom
(iEdgβπΊ) β πΉ β Word dom
(iEdgβπΊ))) |
5 | | idd 24 |
. . . 4
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β π:(0...(β―βπΉ))βΆ(VtxβπΊ))) |
6 | | ifpprsnss 4726 |
. . . . . 6
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) |
7 | 6 | a1i 11 |
. . . . 5
β’ (((πΊ β V β§ πΉ β V β§ π β V) β§ π β
(0..^(β―βπΉ)))
β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
8 | 7 | ralimdva 3161 |
. . . 4
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
9 | 4, 5, 8 | 3anim123d 1444 |
. . 3
β’ ((πΊ β V β§ πΉ β V β§ π β V) β ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
10 | 1, 2 | isupwlk 46124 |
. . 3
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
11 | 1, 2 | iswlk 28600 |
. . 3
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
12 | 9, 10, 11 | 3imtr4d 294 |
. 2
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(UPWalksβπΊ)π β πΉ(WalksβπΊ)π)) |
13 | 3, 12 | mpcom 38 |
1
β’ (πΉ(UPWalksβπΊ)π β πΉ(WalksβπΊ)π) |