Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 eupth0.v ⊢ V = Vtx ⁡ G
2 eupth0.i ⊢ I = iEdg ⁡ G
3 eupthres.d ⊢ φ → F EulerPaths ⁡ G P
4 eupthres.n ⊢ φ → N ∈ 0 ..^ F
5 eupthres.e ⊢ φ → iEdg ⁡ S = I ↾ F 0 ..^ N
6 eupthres.h ⊢ H = F prefix N
7 eupthres.q ⊢ Q = P ↾ 0 … N
8 eupthres.s ⊢ Vtx ⁡ S = V
9 eupthistrl ⊢ F EulerPaths ⁡ G P → F Trails ⁡ G P
10 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
11 3 9 10 3syl ⊢ φ → F Walks ⁡ G P
12 8 a1i ⊢ φ → Vtx ⁡ S = V
13 1 2 11 4 12 5 6 7 wlkres ⊢ φ → H Walks ⁡ S Q
14 3 9 syl ⊢ φ → F Trails ⁡ G P
15 1 2 14 4 6 trlreslem ⊢ φ → H : 0 ..^ H ⟶ 1-1 onto dom ⁡ I ↾ F 0 ..^ N
16 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
17 16 iseupthf1o ⊢ H EulerPaths ⁡ S Q ↔ H Walks ⁡ S Q ∧ H : 0 ..^ H ⟶ 1-1 onto dom ⁡ iEdg ⁡ S
18 5 dmeqd ⊢ φ → dom ⁡ iEdg ⁡ S = dom ⁡ I ↾ F 0 ..^ N
19 18 f1oeq3d ⊢ φ → H : 0 ..^ H ⟶ 1-1 onto dom ⁡ iEdg ⁡ S ↔ H : 0 ..^ H ⟶ 1-1 onto dom ⁡ I ↾ F 0 ..^ N
20 19 anbi2d ⊢ φ → H Walks ⁡ S Q ∧ H : 0 ..^ H ⟶ 1-1 onto dom ⁡ iEdg ⁡ S ↔ H Walks ⁡ S Q ∧ H : 0 ..^ H ⟶ 1-1 onto dom ⁡ I ↾ F 0 ..^ N
21 17 20 bitrid ⊢ φ → H EulerPaths ⁡ S Q ↔ H Walks ⁡ S Q ∧ H : 0 ..^ H ⟶ 1-1 onto dom ⁡ I ↾ F 0 ..^ N
22 13 15 21 mpbir2and ⊢ φ → H EulerPaths ⁡ S Q