Theorem eupthres

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

	Ref	Expression
Hypotheses	eupth0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	eupth0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	eupthres.d	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
	eupthres.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
	eupthres.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
	eupthres.h	$$⊢H=F\mathrm{prefix}N$$
	eupthres.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
	eupthres.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
Assertion	eupthres	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$

Proof

Step	Hyp	Ref	Expression
1		eupth0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eupth0.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eupthres.d	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
4		eupthres.n	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
5		eupthres.e	$$⊢\phi \to \mathrm{iEdg}\left(S\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
6		eupthres.h	$$⊢H=F\mathrm{prefix}N$$
7		eupthres.q	$$⊢Q={P\upharpoonright }_{\left(0\dots N\right)}$$
8		eupthres.s	$$⊢\mathrm{Vtx}\left(S\right)=V$$
9		eupthistrl	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$
10		trliswlk	$$⊢F\mathrm{Trails}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
11	3 9 10	3syl	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
12	8	a1i	$$⊢\phi \to \mathrm{Vtx}\left(S\right)=V$$
13	1 2 11 4 12 5 6 7	wlkres	$$⊢\phi \to H\mathrm{Walks}\left(S\right)Q$$
14	3 9	syl	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
15	1 2 14 4 6	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)$$
16		eqid	$$⊢\mathrm{iEdg}\left(S\right)=\mathrm{iEdg}\left(S\right)$$
17	16	iseupthf1o	$$⊢H\mathrm{EulerPaths}\left(S\right)Q\leftrightarrow \left(H\mathrm{Walks}\left(S\right)Q\wedge H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(S\right)\right)$$
18	5	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(S\right)=\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)$$
19	18	f1oeq3d	$$⊢\phi \to \left(H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(S\right)\leftrightarrow H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\right)$$
20	19	anbi2d	$$⊢\phi \to \left(\left(H\mathrm{Walks}\left(S\right)Q\wedge H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(S\right)\right)\leftrightarrow \left(H\mathrm{Walks}\left(S\right)Q\wedge H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\right)\right)$$
21	17 20	bitrid	$$⊢\phi \to \left(H\mathrm{EulerPaths}\left(S\right)Q\leftrightarrow \left(H\mathrm{Walks}\left(S\right)Q\wedge H:\left(0..^\left|H\right|\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\right)\right)\right)$$
22	13 15 21	mpbir2and	$$⊢\phi \to H\mathrm{EulerPaths}\left(S\right)Q$$