This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Vtx ⁡ G
trlres.i ⊢ I = iEdg ⁡ G
trlres.d ⊢ φ → F Trails ⁡ G P
trlres.n ⊢ φ → N ∈ 0 ..^ F
trlres.h ⊢ H = F prefix N
trlres.s ⊢ φ → Vtx ⁡ S = V
trlres.e ⊢ φ → iEdg ⁡ S = I ↾ F 0 ..^ N
trlres.q ⊢ Q = P ↾ 0 … N
Assertion trlres ⊢ φ → H Trails ⁡ S Q

Proof

Step Hyp Ref Expression
1 trlres.v ⊢ V = Vtx ⁡ G
2 trlres.i ⊢ I = iEdg ⁡ G
3 trlres.d ⊢ φ → F Trails ⁡ G P
4 trlres.n ⊢ φ → N ∈ 0 ..^ F
5 trlres.h ⊢ H = F prefix N
6 trlres.s ⊢ φ → Vtx ⁡ S = V
7 trlres.e ⊢ φ → 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 ⊢ φ → F Walks ⁡ G P
11 1 2 10 4 6 7 5 8 wlkres ⊢ φ → H Walks ⁡ S Q
12 1 2 3 4 5 trlreslem ⊢ φ → 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 -1
15 14 simprbi ⊢ H : 0 ..^ H ⟶ 1-1 dom ⁡ I ↾ F 0 ..^ N → Fun ⁡ H -1
16 12 13 15 3syl ⊢ φ → Fun ⁡ H -1
17 istrl ⊢ H Trails ⁡ S Q ↔ H Walks ⁡ S Q ∧ Fun ⁡ H -1
18 11 16 17 sylanbrc ⊢ φ → H Trails ⁡ S Q