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 25 30 syl 
 |-  ( F ( EulerPaths ` G ) P -> F e. Word dom I )
32 lencl 
 |-  ( F e. Word dom I -> ( # ` F ) e. NN0 )
33 9 eleq1i 
 |-  ( N e. NN0 <-> ( # ` F ) e. NN0 )
34 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
35 33 34 sylbir 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... N ) )
36 32 35 syl 
 |-  ( F e. Word dom I -> 0 e. ( 0 ... N ) )
37 8 31 36 3syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
38 24 29 37 rspcdva 
 |-  ( ph -> ( Q ` 0 ) = ( P ` 0 ) )
39 38 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` 0 ) = ( P ` 0 ) )
40 17 eqcomd 
 |-  ( ph -> ( P ` 0 ) = C )
41 40 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( P ` 0 ) = C )
42 14 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> Q = ( P u. { <. ( N + 1 ) , C >. } ) )
43 13 fveq2i 
 |-  ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) )
44 43 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` H ) = ( # ` ( F u. { <. N , B >. } ) ) )
45 wrdfin 
 |-  ( F e. Word dom I -> F e. Fin )
46 30 45 syl 
 |-  ( F ( Walks ` G ) P -> F e. Fin )
47 8 25 46 3syl 
 |-  ( ph -> F e. Fin )
48 47 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> F e. Fin )
49 snfi 
 |-  { <. N , B >. } e. Fin
50 49 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> { <. N , B >. } e. Fin )
51 wrddm 
 |-  ( F e. Word dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
52 8 31 51 3syl 
 |-  ( ph -> dom F = ( 0 ..^ ( # ` F ) ) )
53 fzonel 
 |-  -. ( # ` F ) e. ( 0 ..^ ( # ` F ) )
54 53 a1i 
 |-  ( ph -> -. ( # ` F ) e. ( 0 ..^ ( # ` F ) ) )
55 9 eleq1i 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. ( 0 ..^ ( # ` F ) ) )
56 54 55 sylnibr 
 |-  ( ph -> -. N e. ( 0 ..^ ( # ` F ) ) )
57 eleq2 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( N e. dom F <-> N e. ( 0 ..^ ( # ` F ) ) ) )
58 57 notbid 
 |-  ( dom F = ( 0 ..^ ( # ` F ) ) -> ( -. N e. dom F <-> -. N e. ( 0 ..^ ( # ` F ) ) ) )
59 56 58 syl5ibrcom 
 |-  ( ph -> ( dom F = ( 0 ..^ ( # ` F ) ) -> -. N e. dom F ) )
60 9 fvexi 
 |-  N e. _V
61 60 a1i 
 |-  ( ph -> N e. _V )
62 61 5 opeldmd 
 |-  ( ph -> ( <. N , B >. e. F -> N e. dom F ) )
63 59 62 nsyld 
 |-  ( ph -> ( dom F = ( 0 ..^ ( # ` F ) ) -> -. <. N , B >. e. F ) )
64 52 63 mpd 
 |-  ( ph -> -. <. N , B >. e. F )
65 64 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> -. <. N , B >. e. F )
66 disjsn 
 |-  ( ( F i^i { <. N , B >. } ) = (/) <-> -. <. N , B >. e. F )
67 65 66 sylibr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( F i^i { <. N , B >. } ) = (/) )
68 hashun 
 |-  ( ( F e. Fin /\ { <. N , B >. } e. Fin /\ ( F i^i { <. N , B >. } ) = (/) ) -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + ( # ` { <. N , B >. } ) ) )
69 48 50 67 68 syl3anc 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` ( F u. { <. N , B >. } ) ) = ( ( # ` F ) + ( # ` { <. N , B >. } ) ) )
70 9 eqcomi 
 |-  ( # ` F ) = N
71 opex 
 |-  <. N , B >. e. _V
72 hashsng 
 |-  ( <. N , B >. e. _V -> ( # ` { <. N , B >. } ) = 1 )
73 71 72 ax-mp 
 |-  ( # ` { <. N , B >. } ) = 1
74 70 73 oveq12i 
 |-  ( ( # ` F ) + ( # ` { <. N , B >. } ) ) = ( N + 1 )
75 74 a1i 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( # ` F ) + ( # ` { <. N , B >. } ) ) = ( N + 1 ) )
76 44 69 75 3eqtrd 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( # ` H ) = ( N + 1 ) )
77 42 76 fveq12d 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` ( # ` H ) ) = ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) )
78 ovexd 
 |-  ( ph -> ( N + 1 ) e. _V )
79 1 2 3 4 5 6 7 26 9 wlkp1lem1 
 |-  ( ph -> -. ( N + 1 ) e. dom P )
80 78 6 79 3jca 
 |-  ( ph -> ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) )
81 80 adantr 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) )
82 fsnunfv 
 |-  ( ( ( N + 1 ) e. _V /\ C e. V /\ -. ( N + 1 ) e. dom P ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
83 81 82 syl 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( ( P u. { <. ( N + 1 ) , C >. } ) ` ( N + 1 ) ) = C )
84 77 83 eqtr2d 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> C = ( Q ` ( # ` H ) ) )
85 39 41 84 3eqtrd 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( Q ` 0 ) = ( Q ` ( # ` H ) ) )
86 iscrct 
 |-  ( H ( Circuits ` S ) Q <-> ( H ( Trails ` S ) Q /\ ( Q ` 0 ) = ( Q ` ( # ` H ) ) ) )
87 21 85 86 sylanbrc 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> H ( Circuits ` S ) Q )
88 19 87 jca 
 |-  ( ( ph /\ H ( EulerPaths ` S ) Q ) -> ( H ( EulerPaths ` S ) Q /\ H ( Circuits ` S ) Q ) )
89 18 88 mpdan 
 |-  ( ph -> ( H ( EulerPaths ` S ) Q /\ H ( Circuits ` S ) Q ) )