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 
|- ( ph -> F ( EulerPaths ` G ) P )
eupthres.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
eupthres.e 
|- ( ph -> ( 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 
|- ( ph -> H ( EulerPaths ` S ) Q )

Proof

Step Hyp Ref Expression
1 eupth0.v 
 |-  V = ( Vtx ` G )
2 eupth0.i 
 |-  I = ( iEdg ` G )
3 eupthres.d 
 |-  ( ph -> F ( EulerPaths ` G ) P )
4 eupthres.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 eupthres.e 
 |-  ( ph -> ( 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 
 |-  ( ph -> F ( Walks ` G ) P )
12 8 a1i 
 |-  ( ph -> ( Vtx ` S ) = V )
13 1 2 11 4 12 5 6 7 wlkres 
 |-  ( ph -> H ( Walks ` S ) Q )
14 3 9 syl 
 |-  ( ph -> F ( Trails ` G ) P )
15 1 2 14 4 6 trlreslem 
 |-  ( ph -> 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 
 |-  ( ph -> dom ( iEdg ` S ) = dom ( I |` ( F " ( 0 ..^ N ) ) ) )
19 18 f1oeq3d 
 |-  ( ph -> ( H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( iEdg ` S ) <-> H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) ) )
20 19 anbi2d 
 |-  ( ph -> ( ( 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 syl5bb 
 |-  ( ph -> ( H ( EulerPaths ` S ) Q <-> ( H ( Walks ` S ) Q /\ H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0 ..^ N ) ) ) ) ) )
22 13 15 21 mpbir2and 
 |-  ( ph -> H ( EulerPaths ` S ) Q )