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

Proof

Step	Hyp	Ref	Expression
1		trlres.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		trlres.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		trlres.d	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
4		trlres.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5		trlres.h	⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
6		trlres.s	⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
7		trlres.e	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
8		trlres.q	⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
9		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10	3 9	syl	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
11	1 2 10 4 6 7 5 8	wlkres	⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )
12	1 2 3 4 5	trlreslem	⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
13		f1of1	⊢ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
14		df-f1	⊢ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ↔ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∧ Fun ◡ 𝐻 ) )
15	14	simprbi	⊢ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) → Fun ◡ 𝐻 )
16	12 13 15	3syl	⊢ ( 𝜑 → Fun ◡ 𝐻 )
17		istrl	⊢ ( 𝐻 ( Trails ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ Fun ◡ 𝐻 ) )
18	11 16 17	sylanbrc	⊢ ( 𝜑 → 𝐻 ( Trails ‘ 𝑆 ) 𝑄 )