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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	eupth0.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	eupthres.d	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
	eupthres.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
	eupthres.e	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
	eupthres.h	⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
	eupthres.q	⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
	eupthres.s	⊢ ( Vtx ‘ 𝑆 ) = 𝑉
Assertion	eupthres	⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		eupth0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eupth0.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		eupthres.d	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
4		eupthres.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5		eupthres.e	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
6		eupthres.h	⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
7		eupthres.q	⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
8		eupthres.s	⊢ ( Vtx ‘ 𝑆 ) = 𝑉
9		eupthistrl	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
11	3 9 10	3syl	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
12	8	a1i	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
13	1 2 11 4 12 5 6 7	wlkres	⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )
14	3 9	syl	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
15	1 2 14 4 6	trlreslem	⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
16		eqid	⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
17	16	iseupthf1o	⊢ ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) )
18	5	dmeqd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝑆 ) = dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
19	18	f1oeq3d	⊢ ( 𝜑 → ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ↔ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) )
20	19	anbi2d	⊢ ( 𝜑 → ( ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) ) )
21	17 20	bitrid	⊢ ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) ) )
22	13 15 21	mpbir2and	⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

Metamath Proof Explorer

Theorem eupthres

Proof