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 = ( Vtx ` G )
	trlres.i	|- I = ( iEdg ` G )
	trlres.d	|- ( ph -> F ( Trails ` G ) P )
	trlres.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
	trlres.h	|- H = ( F prefix N )
	trlres.s	|- ( ph -> ( Vtx ` S ) = V )
	trlres.e	|- ( ph -> ( iEdg ` S ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
	trlres.q	|- Q = ( P |` ( 0 ... N ) )
Assertion	trlres	|- ( ph -> H ( Trails ` S ) Q )

Proof

Step	Hyp	Ref	Expression
1		trlres.v	|- V = ( Vtx ` G )
2		trlres.i	|- I = ( iEdg ` G )
3		trlres.d	|- ( ph -> F ( Trails ` G ) P )
4		trlres.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5		trlres.h	|- H = ( F prefix N )
6		trlres.s	|- ( ph -> ( Vtx ` S ) = V )
7		trlres.e	|- ( ph -> ( iEdg ` S ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
8		trlres.q	|- Q = ( P |` ( 0 ... N ) )
9		trliswlk	|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
10	3 9	syl	|- ( ph -> F ( Walks ` G ) P )
11	1 2 10 4 6 7 5 8	wlkres	|- ( ph -> H ( Walks ` S ) Q )
12	1 2 3 4 5	trlreslem	|- ( ph -> H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) )
13		f1of1	|- ( H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) -> H : ( 0 ..^ ( # ` H ) ) -1-1-> dom ( I |` ( F " ( 0 ..^ N ) ) ) )
14		df-f1	|- ( H : ( 0 ..^ ( # ` H ) ) -1-1-> dom ( I |` ( F " ( 0 ..^ N ) ) ) <-> ( H : ( 0 ..^ ( # ` H ) ) --> dom ( I |` ( F " ( 0 ..^ N ) ) ) /\ Fun `' H ) )
15	14	simprbi	|- ( H : ( 0 ..^ ( # ` H ) ) -1-1-> dom ( I |` ( F " ( 0 ..^ N ) ) ) -> Fun `' H )
16	12 13 15	3syl	|- ( ph -> Fun `' H )
17		istrl	|- ( H ( Trails ` S ) Q <-> ( H ( Walks ` S ) Q /\ Fun `' H ) )
18	11 16 17	sylanbrc	|- ( ph -> H ( Trails ` S ) Q )