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 )

Metamath Proof Explorer

Theorem trlres

Proof