Metamath Proof Explorer


Theorem ewlkprop

Description: Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i I=iEdgG
Assertion ewlkprop FGEdgWalksSGVS0*FWorddomIk1..^FSIFk1IFk

Proof

Step Hyp Ref Expression
1 ewlksfval.i I=iEdgG
2 df-ewlks EdgWalks=gV,s0*f|[˙iEdgg/i]˙fWorddomik1..^fsifk1ifk
3 2 elmpocl FGEdgWalksSGVS0*
4 simpr FGEdgWalksSGVS0*GVS0*
5 1 isewlk GVS0*FGEdgWalksSFGEdgWalksSFWorddomIk1..^FSIFk1IFk
6 5 3expa GVS0*FGEdgWalksSFGEdgWalksSFWorddomIk1..^FSIFk1IFk
7 6 biimpd GVS0*FGEdgWalksSFGEdgWalksSFWorddomIk1..^FSIFk1IFk
8 7 expcom FGEdgWalksSGVS0*FGEdgWalksSFWorddomIk1..^FSIFk1IFk
9 8 pm2.43a FGEdgWalksSGVS0*FWorddomIk1..^FSIFk1IFk
10 9 imp FGEdgWalksSGVS0*FWorddomIk1..^FSIFk1IFk
11 3anass GVS0*FWorddomIk1..^FSIFk1IFkGVS0*FWorddomIk1..^FSIFk1IFk
12 4 10 11 sylanbrc FGEdgWalksSGVS0*GVS0*FWorddomIk1..^FSIFk1IFk
13 3 12 mpdan FGEdgWalksSGVS0*FWorddomIk1..^FSIFk1IFk