Metamath Proof Explorer

Theorem eupth2eucrct

Description: Append one path segment to an Eulerian path <. F , P >. which may not be an (Eulerian) circuit to become an Eulerian circuit <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by AV, 11-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 } )
eupth2eucrct.c 
|- ( ph -> C = ( P ` 0 ) )
Assertion eupth2eucrct 
|- ( ph -> ( H ( EulerPaths ` S ) Q /\ H ( Circuits ` 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 eupth2eucrct.c 
 |-  ( ph -> C = ( P ` 0 ) )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 eupthp1 
 |-  ( ph -> H ( EulerPaths ` S ) Q )
19 simpr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> H ( EulerPaths ` S ) Q )
20 eupthistrl 
 |-  ( H ( EulerPaths ` S ) Q -> H ( Trails ` S ) Q )
21 20 adantl 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> H ( Trails ` S ) Q )
22 fveq2 
 |-  ( k = 0 -> ( Q ` k ) = ( Q ` 0 ) )
23 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
24 22 23 eqeq12d 
 |-  ( k = 0 -> ( ( Q ` k ) = ( P ` k ) <-> ( Q ` 0 ) = ( P ` 0 ) ) )
25 eupthiswlk 
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
26 8 25 syl 
 |-  ( ph -> F ( Walks ` G ) P )
27 12 a1i 
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
28 15 a1i 
 |-  ( ph -> ( Vtx ` S ) = V )
29 1 2 3 4 5 6 7 26 9 10 11 27 13 14 28 wlkp1lem5 
 |-  ( ph -> A. k e. ( 0 ... N ) ( Q ` k ) = ( P ` k ) )
30 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
31 lencl 
 |-  ( F e. Word dom I -> ( # ` F ) e. NN0 )
32 9 eleq1i 
 |-  ( N e. NN0 <-> ( # ` F ) e. NN0 )
33 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
34 32 33 sylbir 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... N ) )
35 31 34 syl 
 |-  ( F e. Word dom I -> 0 e. ( 0 ... N ) )
36 8 25 30 35 4syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
37 24 29 36 rspcdva 
 |-  ( ph -> ( Q ` 0 ) = ( P ` 0 ) )
38 37 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` 0 ) = ( P ` 0 ) )
39 17 eqcomd 
 |-  ( ph -> ( P ` 0 ) = C )
40 39 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( P ` 0 ) = C )
41 14 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> Q = ( P u. { <. ( N + 1 ) , C >. } ) )
42 13 fveq2i 
 |-  ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) )
43 42 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) ) )
44 wrdfin 
 |-  ( F e. Word dom I -> F e. Fin )
45 8 25 30 44 4syl 
 |-  ( ph -> F e. Fin )
46 45 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> F e. Fin )
47 snfi 
 |-  { <. N , B >. } e. Fin
48 47 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> { <. N , B >. } e. Fin )
49 wrddm 
 |-  ( F e. Word dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
50 8 25 30 49 4syl 
 |-  ( ph -> dom F = ( 0 ..^ ( # ` F ) ) )
51 fzonel 
 |-  -. ( # ` F ) e. ( 0 ..^ ( # ` F ) )
52 51 a1i 
 |-  ( ph -> -. ( # ` F ) e. ( 0 ..^ ( # ` F ) ) )
53 9 eleq1i 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. ( 0 ..^ ( # ` F ) ) )
54 52 53 sylnibr 
 |-  ( ph -> -. N e. ( 0 ..^ ( # ` F ) ) )
55 eleq2 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( N e. dom F <-> N e. ( 0 ..^ ( # ` F ) ) ) )
56 55 notbid 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( -. N e. dom F <-> -. N e. ( 0 ..^ ( # ` F ) ) ) )
57 54 56 syl5ibrcom 
 |-  ( ph -> ( dom F = ( 0 ..^ ( # ` F ) ) -> -. N e. dom F ) )
58 9 fvexi 
 |-  N e. _V
59 58 a1i 
 |-  ( ph -> N e. _V )
60 59 5 opeldmd 
 |-  ( ph -> ( <. N , B >. e. F -> N e. dom F ) )
61 57 60 nsyld 
 |-  ( ph -> ( dom F = ( 0 ..^ ( # ` F ) ) -> -. <. N , B >. e. F ) )
62 50 61 mpd 
 |-  ( ph -> -. <. N , B >. e. F )
63 62 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> -. <. N , B >. e. F )
64 disjsn 
 |-  ( ( F i^i { <. N , B >. } ) = (/) <-> -. <. N , B >. e. F )
65 63 64 sylibr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( F i^i { <. N , B >. } ) = (/) )
66 hashun 
 |-  ( ( F e. Fin /\ { <. N , B >. } e. Fin /\ ( F i^i { <. N , B >. } ) = (/) ) -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + ( # ` { <. N , B >. } ) ) )
67 46 48 65 66 syl3anc 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + ( # ` { <. N , B >. } ) ) )
68 9 eqcomi 
 |-  ( # ` F ) = N
69 opex 
 |-  <. N , B >. e. _V
70 hashsng 
 |-  ( <. N , B >. e. _V -> ( # ` { <. N , B >. } ) = 1 )
71 69 70 ax-mp 
 |-  ( # ` { <. N , B >. } ) = 1
72 68 71 oveq12i 
 |-  ( ( # ` F ) + ( # ` { <. N , B >. } ) ) = ( N + 1 )
73 72 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( # ` F ) + ( # ` { <. N , B >. } ) ) = ( N + 1 ) )
74 43 67 73 3eqtrd 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` H ) = ( N + 1 ) )
75 41 74 fveq12d 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` ( # ` H ) ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) )
76 ovexd 
 |-  ( ph -> ( N + 1 ) e. _V )
77 1 2 3 4 5 6 7 26 9 wlkp1lem1 
 |-  ( ph -> -. ( N + 1 ) e. dom P )
78 76 6 77 3jca 
 |-  ( ph -> ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) )
79 78 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) )
80 fsnunfv 
 |-  ( ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
81 79 80 syl 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
82 75 81 eqtr2d 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> C = ( Q ` ( # ` H ) ) )
83 38 40 82 3eqtrd 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` 0 ) = ( Q ` ( # ` H ) ) )
84 iscrct 
 |-  ( H ( Circuits ` S ) Q <-> ( H ( Trails ` S ) Q /\ ( Q ` 0 ) = ( Q ` ( # ` H ) ) ) )
85 21 83 84 sylanbrc 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> H ( Circuits ` S ) Q )
86 19 85 jca 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( H ( EulerPaths ` S ) Q /\ H ( Circuits ` S ) Q ) )
87 18 86 mpdan 
 |-  ( ph -> ( H ( EulerPaths ` S ) Q /\ H ( Circuits ` S ) Q ) )