Metamath Proof Explorer

Theorem eupthp1

Description: Append one path segment to an Eulerian path <. F , P >. to become an Eulerian path <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 7-Mar-2021) (Proof shortened by AV, 30-Oct-2021) (Revised by AV, 8-Apr-2024)

Ref Expression
Hypotheses eupthp1.v 
|- V = ( Vtx ` G )
eupthp1.i 
|- I = ( iEdg ` G )
eupthp1.f 
|- ( ph -> Fun I )
eupthp1.a 
|- ( ph -> I e. Fin )
eupthp1.b 
|- ( ph -> B e. W )
eupthp1.c 
|- ( ph -> C e. V )
eupthp1.d 
|- ( ph -> -. B e. dom I )
eupthp1.p 
|- ( ph -> F ( EulerPaths ` G ) P )
eupthp1.n 
|- N = ( # ` F )
eupthp1.e 
|- ( ph -> E e. ( Edg ` G ) )
eupthp1.x 
|- ( ph -> { ( P ` N ) , C } C_ E )
eupthp1.u 
|- ( iEdg ` S ) = ( I u. { <. B , E >. } )
eupthp1.h 
|- H = ( F u. { <. N , B >. } )
eupthp1.q 
|- Q = ( P u. { <. ( N + 1 ) , C >. } )
eupthp1.s 
|- ( Vtx ` S ) = V
eupthp1.l 
|- ( ( ph /\ C = ( P ` N ) ) -> E = { C } )
Assertion eupthp1 
|- ( ph -> H ( EulerPaths ` S ) Q )

Proof

Step Hyp Ref Expression
1 eupthp1.v 
 |-  V = ( Vtx ` G )
2 eupthp1.i 
 |-  I = ( iEdg ` G )
3 eupthp1.f 
 |-  ( ph -> Fun I )
4 eupthp1.a 
 |-  ( ph -> I e. Fin )
5 eupthp1.b 
 |-  ( ph -> B e. W )
6 eupthp1.c 
 |-  ( ph -> C e. V )
7 eupthp1.d 
 |-  ( ph -> -. B e. dom I )
8 eupthp1.p 
 |-  ( ph -> F ( EulerPaths ` G ) P )
9 eupthp1.n 
 |-  N = ( # ` F )
10 eupthp1.e 
 |-  ( ph -> E e. ( Edg ` G ) )
11 eupthp1.x 
 |-  ( ph -> { ( P ` N ) , C } C_ E )
12 eupthp1.u 
 |-  ( iEdg ` S ) = ( I u. { <. B , E >. } )
13 eupthp1.h 
 |-  H = ( F u. { <. N , B >. } )
14 eupthp1.q 
 |-  Q = ( P u. { <. ( N + 1 ) , C >. } )
15 eupthp1.s 
 |-  ( Vtx ` S ) = V
16 eupthp1.l 
 |-  ( ( ph /\ C = ( P ` N ) ) -> E = { C } )
17 eupthiswlk 
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
18 8 17 syl 
 |-  ( ph -> F ( Walks ` G ) P )
19 12 a1i 
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
20 15 a1i 
 |-  ( ph -> ( Vtx ` S ) = V )
21 1 2 3 4 5 6 7 18 9 10 11 19 13 14 20 16 wlkp1 
 |-  ( ph -> H ( Walks ` S ) Q )
22 2 eupthi 
 |-  ( F ( EulerPaths ` G ) P -> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) )
23 9 eqcomi 
 |-  ( # ` F ) = N
24 23 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N )
25 f1oeq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I <-> F : ( 0 ..^ N ) -1-1-onto-> dom I ) )
26 24 25 ax-mp 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I <-> F : ( 0 ..^ N ) -1-1-onto-> dom I )
27 26 biimpi 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> F : ( 0 ..^ N ) -1-1-onto-> dom I )
28 27 adantl 
 |-  ( ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) -> F : ( 0 ..^ N ) -1-1-onto-> dom I )
29 8 22 28 3syl 
 |-  ( ph -> F : ( 0 ..^ N ) -1-1-onto-> dom I )
30 9 fvexi 
 |-  N e. _V
31 f1osng 
 |-  ( ( N e. _V /\ B e. W ) -> { <. N , B >. } : { N } -1-1-onto-> { B } )
32 30 5 31 sylancr 
 |-  ( ph -> { <. N , B >. } : { N } -1-1-onto-> { B } )
33 dmsnopg 
 |-  ( E e. ( Edg ` G ) -> dom { <. B , E >. } = { B } )
34 10 33 syl 
 |-  ( ph -> dom { <. B , E >. } = { B } )
35 34 f1oeq3d 
 |-  ( ph -> ( { <. N , B >. } : { N } -1-1-onto-> dom { <. B , E >. } <-> { <. N , B >. } : { N } -1-1-onto-> { B } ) )
36 32 35 mpbird 
 |-  ( ph -> { <. N , B >. } : { N } -1-1-onto-> dom { <. B , E >. } )
37 fzodisjsn 
 |-  ( ( 0 ..^ N ) i^i { N } ) = (/)
38 37 a1i 
 |-  ( ph -> ( ( 0 ..^ N ) i^i { N } ) = (/) )
39 34 ineq2d 
 |-  ( ph -> ( dom I i^i dom { <. B , E >. } ) = ( dom I i^i { B } ) )
40 disjsn 
 |-  ( ( dom I i^i { B } ) = (/) <-> -. B e. dom I )
41 7 40 sylibr 
 |-  ( ph -> ( dom I i^i { B } ) = (/) )
42 39 41 eqtrd 
 |-  ( ph -> ( dom I i^i dom { <. B , E >. } ) = (/) )
43 f1oun 
 |-  ( ( ( F : ( 0 ..^ N ) -1-1-onto-> dom I /\ { <. N , B >. } : { N } -1-1-onto-> dom { <. B , E >. } ) /\ ( ( ( 0 ..^ N ) i^i { N } ) = (/) /\ ( dom I i^i dom { <. B , E >. } ) = (/) ) ) -> ( F u. { <. N , B >. } ) : ( ( 0 ..^ N ) u. { N } ) -1-1-onto-> ( dom I u. dom { <. B , E >. } ) )
44 29 36 38 42 43 syl22anc 
 |-  ( ph -> ( F u. { <. N , B >. } ) : ( ( 0 ..^ N ) u. { N } ) -1-1-onto-> ( dom I u. dom { <. B , E >. } ) )
45 13 a1i 
 |-  ( ph -> H = ( F u. { <. N , B >. } ) )
46 1 2 3 4 5 6 7 18 9 10 11 19 13 wlkp1lem2 
 |-  ( ph -> ( # ` H ) = ( N + 1 ) )
47 46 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ ( N + 1 ) ) )
48 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
49 9 eleq1i 
 |-  ( N e. NN0 <-> ( # ` F ) e. NN0 )
50 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
51 49 50 sylbb1 
 |-  ( ( # ` F ) e. NN0 -> N e. ( ZZ>= ` 0 ) )
52 48 51 syl 
 |-  ( F ( Walks ` G ) P -> N e. ( ZZ>= ` 0 ) )
53 8 17 52 3syl 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
54 fzosplitsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
55 53 54 syl 
 |-  ( ph -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
56 47 55 eqtrd 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( ( 0 ..^ N ) u. { N } ) )
57 dmun 
 |-  dom ( I u. { <. B , E >. } ) = ( dom I u. dom { <. B , E >. } )
58 57 a1i 
 |-  ( ph -> dom ( I u. { <. B , E >. } ) = ( dom I u. dom { <. B , E >. } ) )
59 45 56 58 f1oeq123d 
 |-  ( ph -> ( H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I u. { <. B , E >. } ) <-> ( F u. { <. N , B >. } ) : ( ( 0 ..^ N ) u. { N } ) -1-1-onto-> ( dom I u. dom { <. B , E >. } ) ) )
60 44 59 mpbird 
 |-  ( ph -> H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I u. { <. B , E >. } ) )
61 12 eqcomi 
 |-  ( I u. { <. B , E >. } ) = ( iEdg ` S )
62 61 iseupthf1o 
 |-  ( H ( EulerPaths ` S ) Q <-> ( H ( Walks ` S ) Q /\ H : ( 0 ..^ ( # ` H ) ) -1-1-onto-> dom ( I u. { <. B , E >. } ) ) )
63 21 60 62 sylanbrc 
 |-  ( ph -> H ( EulerPaths ` S ) Q )