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=\mathrm{Vtx}\left(G\right)$$
	trlres.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	trlres.d	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
	trlres.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
	trlres.h	$$⊢H=F\mathrm{prefix}N$$
	trlres.s	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
	trlres.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
	trlres.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
Assertion	trlres	$$⊢\phi \to H\mathrm{Trails}\left(S\right)Q$$

Proof

Step	Hyp	Ref	Expression
1		trlres.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		trlres.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		trlres.d	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
4		trlres.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
5		trlres.h	$$⊢H=F\mathrm{prefix}N$$
6		trlres.s	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
7		trlres.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
8		trlres.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
9		trliswlk	$$⊢F\mathrm{Trails}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
10	3 9	syl	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
11	1 2 10 4 6 7 5 8	wlkres	$$⊢\phi \to H\mathrm{Walks}\left(S\right)Q$$
12	1 2 3 4 5	trlreslem	$$⊢\phi \to H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)$$
13		f1of1	$$⊢H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\to H:\left(0..^\left|H\right|\right)\underset{1-1}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)$$
14		df-f1	$$⊢H:\left(0..^\left|H\right|\right)\underset{1-1}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\leftrightarrow \left(H:\left(0..^\left|H\right|\right)⟶\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\wedge \mathrm{Fun}{H}^{-1}\right)$$
15	14	simprbi	$$⊢H:\left(0..^\left|H\right|\right)\underset{1-1}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\to \mathrm{Fun}{H}^{-1}$$
16	12 13 15	3syl	$$⊢\phi \to \mathrm{Fun}{H}^{-1}$$
17		istrl	$$⊢H\mathrm{Trails}\left(S\right)Q\leftrightarrow \left(H\mathrm{Walks}\left(S\right)Q\wedge \mathrm{Fun}{H}^{-1}\right)$$
18	11 16 17	sylanbrc	$$⊢\phi \to H\mathrm{Trails}\left(S\right)Q$$