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 syl5bb ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ) ) )
22 13 15 21 mpbir2and ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )