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

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 ⊢ 𝑉 = ( 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 ‘ 𝑆 ) 𝑄 )