Metamath Proof Explorer


Theorem trlres

Description: The restriction <. H , Q >. of a trail <. F , P >. to an initial segment of the trail (of length N ) forms a trail on the subgraph S consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses trlres.v V=VtxG
trlres.i I=iEdgG
trlres.d φFTrailsGP
trlres.n φN0..^F
trlres.h H=FprefixN
trlres.s φVtxS=V
trlres.e φiEdgS=IF0..^N
trlres.q Q=P0N
Assertion trlres φHTrailsSQ

Proof

Step Hyp Ref Expression
1 trlres.v V=VtxG
2 trlres.i I=iEdgG
3 trlres.d φFTrailsGP
4 trlres.n φN0..^F
5 trlres.h H=FprefixN
6 trlres.s φVtxS=V
7 trlres.e φiEdgS=IF0..^N
8 trlres.q Q=P0N
9 trliswlk FTrailsGPFWalksGP
10 3 9 syl φFWalksGP
11 1 2 10 4 6 7 5 8 wlkres φHWalksSQ
12 1 2 3 4 5 trlreslem φH:0..^H1-1 ontodomIF0..^N
13 f1of1 H:0..^H1-1 ontodomIF0..^NH:0..^H1-1domIF0..^N
14 df-f1 H:0..^H1-1domIF0..^NH:0..^HdomIF0..^NFunH-1
15 14 simprbi H:0..^H1-1domIF0..^NFunH-1
16 12 13 15 3syl φFunH-1
17 istrl HTrailsSQHWalksSQFunH-1
18 11 16 17 sylanbrc φHTrailsSQ