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 𝑉 = ( Vtx ‘ 𝐺 )
eupthp1.i 𝐼 = ( iEdg ‘ 𝐺 )
eupthp1.f ( 𝜑 → Fun 𝐼 )
eupthp1.a ( 𝜑𝐼 ∈ Fin )
eupthp1.b ( 𝜑𝐵𝑊 )
eupthp1.c ( 𝜑𝐶𝑉 )
eupthp1.d ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
eupthp1.p ( 𝜑𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
eupthp1.n 𝑁 = ( ♯ ‘ 𝐹 )
eupthp1.e ( 𝜑𝐸 ∈ ( Edg ‘ 𝐺 ) )
eupthp1.x ( 𝜑 → { ( 𝑃𝑁 ) , 𝐶 } ⊆ 𝐸 )
eupthp1.u ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } )
eupthp1.h 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
eupthp1.q 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
eupthp1.s ( Vtx ‘ 𝑆 ) = 𝑉
eupthp1.l ( ( 𝜑𝐶 = ( 𝑃𝑁 ) ) → 𝐸 = { 𝐶 } )
eupth2eucrct.c ( 𝜑𝐶 = ( 𝑃 ‘ 0 ) )
Assertion eupth2eucrct ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ) )

Proof

Step Hyp Ref Expression
1 eupthp1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 eupthp1.i 𝐼 = ( iEdg ‘ 𝐺 )
3 eupthp1.f ( 𝜑 → Fun 𝐼 )
4 eupthp1.a ( 𝜑𝐼 ∈ Fin )
5 eupthp1.b ( 𝜑𝐵𝑊 )
6 eupthp1.c ( 𝜑𝐶𝑉 )
7 eupthp1.d ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8 eupthp1.p ( 𝜑𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
9 eupthp1.n 𝑁 = ( ♯ ‘ 𝐹 )
10 eupthp1.e ( 𝜑𝐸 ∈ ( Edg ‘ 𝐺 ) )
11 eupthp1.x ( 𝜑 → { ( 𝑃𝑁 ) , 𝐶 } ⊆ 𝐸 )
12 eupthp1.u ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } )
13 eupthp1.h 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14 eupthp1.q 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } )
15 eupthp1.s ( Vtx ‘ 𝑆 ) = 𝑉
16 eupthp1.l ( ( 𝜑𝐶 = ( 𝑃𝑁 ) ) → 𝐸 = { 𝐶 } )
17 eupth2eucrct.c ( 𝜑𝐶 = ( 𝑃 ‘ 0 ) )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 eupthp1 ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )
19 simpr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )
20 eupthistrl ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄𝐻 ( Trails ‘ 𝑆 ) 𝑄 )
21 20 adantl ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐻 ( Trails ‘ 𝑆 ) 𝑄 )
22 fveq2 ( 𝑘 = 0 → ( 𝑄𝑘 ) = ( 𝑄 ‘ 0 ) )
23 fveq2 ( 𝑘 = 0 → ( 𝑃𝑘 ) = ( 𝑃 ‘ 0 ) )
24 22 23 eqeq12d ( 𝑘 = 0 → ( ( 𝑄𝑘 ) = ( 𝑃𝑘 ) ↔ ( 𝑄 ‘ 0 ) = ( 𝑃 ‘ 0 ) ) )
25 eupthiswlk ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
26 8 25 syl ( 𝜑𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
27 12 a1i ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
28 15 a1i ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
29 1 2 3 4 5 6 7 26 9 10 11 27 13 14 28 wlkp1lem5 ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑄𝑘 ) = ( 𝑃𝑘 ) )
30 2 wlkf ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐹 ∈ Word dom 𝐼 )
31 lencl ( 𝐹 ∈ Word dom 𝐼 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
32 9 eleq1i ( 𝑁 ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
33 0elfz ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
34 32 33 sylbir ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
35 31 34 syl ( 𝐹 ∈ Word dom 𝐼 → 0 ∈ ( 0 ... 𝑁 ) )
36 8 25 30 35 4syl ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
37 24 29 36 rspcdva ( 𝜑 → ( 𝑄 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
38 37 adantr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
39 17 eqcomd ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝐶 )
40 39 adantr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑃 ‘ 0 ) = 𝐶 )
41 14 a1i ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) )
42 13 fveq2i ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
43 42 a1i ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
44 wrdfin ( 𝐹 ∈ Word dom 𝐼𝐹 ∈ Fin )
45 8 25 30 44 4syl ( 𝜑𝐹 ∈ Fin )
46 45 adantr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐹 ∈ Fin )
47 snfi { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin
48 47 a1i ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin )
49 wrddm ( 𝐹 ∈ Word dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
50 8 25 30 49 4syl ( 𝜑 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
51 fzonel ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
52 51 a1i ( 𝜑 → ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
53 9 eleq1i ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
54 52 53 sylnibr ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
55 eleq2 ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 ∈ dom 𝐹𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
56 55 notbid ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ¬ 𝑁 ∈ dom 𝐹 ↔ ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
57 54 56 syl5ibrcom ( 𝜑 → ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ¬ 𝑁 ∈ dom 𝐹 ) )
58 9 fvexi 𝑁 ∈ V
59 58 a1i ( 𝜑𝑁 ∈ V )
60 59 5 opeldmd ( 𝜑 → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹𝑁 ∈ dom 𝐹 ) )
61 57 60 nsyld ( 𝜑 → ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) )
62 50 61 mpd ( 𝜑 → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
63 62 adantr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
64 disjsn ( ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ ↔ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
65 63 64 sylibr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ )
66 hashun ( ( 𝐹 ∈ Fin ∧ { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin ∧ ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
67 46 48 65 66 syl3anc ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
68 9 eqcomi ( ♯ ‘ 𝐹 ) = 𝑁
69 opex 𝑁 , 𝐵 ⟩ ∈ V
70 hashsng ( ⟨ 𝑁 , 𝐵 ⟩ ∈ V → ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) = 1 )
71 69 70 ax-mp ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) = 1
72 68 71 oveq12i ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( 𝑁 + 1 )
73 72 a1i ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( 𝑁 + 1 ) )
74 43 67 73 3eqtrd ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )
75 41 74 fveq12d ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) = ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) )
76 ovexd ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
77 1 2 3 4 5 6 7 26 9 wlkp1lem1 ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )
78 76 6 77 3jca ( 𝜑 → ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) )
79 78 adantr ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) )
80 fsnunfv ( ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
81 79 80 syl ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
82 75 81 eqtr2d ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐶 = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) )
83 38 40 82 3eqtrd ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) )
84 iscrct ( 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Trails ‘ 𝑆 ) 𝑄 ∧ ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) ) )
85 21 83 84 sylanbrc ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 )
86 19 85 jca ( ( 𝜑𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ) )
87 18 86 mpdan ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ) )