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 25 30 syl ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
32 lencl ⊢ ( 𝐹 ∈ Word dom 𝐼 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
33 9 eleq1i ⊢ ( 𝑁 ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
34 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
35 33 34 sylbir ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
36 32 35 syl ⊢ ( 𝐹 ∈ Word dom 𝐼 → 0 ∈ ( 0 ... 𝑁 ) )
37 8 31 36 3syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
38 24 29 37 rspcdva ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ 0 ) = ( 𝑃 ‘ 0 ) )
40 17 eqcomd ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = 𝐶 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑃 ‘ 0 ) = 𝐶 )
42 14 a1i ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝑄 = ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) )
43 13 fveq2i ⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
44 43 a1i ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
45 wrdfin ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 ∈ Fin )
46 30 45 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Fin )
47 8 25 46 3syl ⊢ ( 𝜑 → 𝐹 ∈ Fin )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐹 ∈ Fin )
49 snfi ⊢ { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin )
51 wrddm ⊢ ( 𝐹 ∈ Word dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
52 8 31 51 3syl ⊢ ( 𝜑 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
53 fzonel ⊢ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
54 53 a1i ⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
55 9 eleq1i ⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
56 54 55 sylnibr ⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
57 eleq2 ⊢ ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 ∈ dom 𝐹 ↔ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
58 57 notbid ⊢ ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ¬ 𝑁 ∈ dom 𝐹 ↔ ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
59 56 58 syl5ibrcom ⊢ ( 𝜑 → ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ¬ 𝑁 ∈ dom 𝐹 ) )
60 9 fvexi ⊢ 𝑁 ∈ V
61 60 a1i ⊢ ( 𝜑 → 𝑁 ∈ V )
62 61 5 opeldmd ⊢ ( 𝜑 → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 → 𝑁 ∈ dom 𝐹 ) )
63 59 62 nsyld ⊢ ( 𝜑 → ( dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) )
64 52 63 mpd ⊢ ( 𝜑 → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
66 disjsn ⊢ ( ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ ↔ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
67 65 66 sylibr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ )
68 hashun ⊢ ( ( 𝐹 ∈ Fin ∧ { ⟨ 𝑁 , 𝐵 ⟩ } ∈ Fin ∧ ( 𝐹 ∩ { ⟨ 𝑁 , 𝐵 ⟩ } ) = ∅ ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
69 48 50 67 68 syl3anc ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
70 9 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
71 opex ⊢ ⟨ 𝑁 , 𝐵 ⟩ ∈ V
72 hashsng ⊢ ( ⟨ 𝑁 , 𝐵 ⟩ ∈ V → ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) = 1 )
73 71 72 ax-mp ⊢ ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) = 1
74 70 73 oveq12i ⊢ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( 𝑁 + 1 )
75 74 a1i ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( 𝑁 + 1 ) )
76 44 69 75 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )
77 42 76 fveq12d ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) = ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) )
78 ovexd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ V )
79 1 2 3 4 5 6 7 26 9 wlkp1lem1 ⊢ ( 𝜑 → ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 )
80 78 6 79 3jca ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) )
82 fsnunfv ⊢ ( ( ( 𝑁 + 1 ) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ ( 𝑁 + 1 ) ∈ dom 𝑃 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
83 81 82 syl ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( ( 𝑃 ∪ { ⟨ ( 𝑁 + 1 ) , 𝐶 ⟩ } ) ‘ ( 𝑁 + 1 ) ) = 𝐶 )
84 77 83 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐶 = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) )
85 39 41 84 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) )
86 iscrct ⊢ ( 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Trails ‘ 𝑆 ) 𝑄 ∧ ( 𝑄 ‘ 0 ) = ( 𝑄 ‘ ( ♯ ‘ 𝐻 ) ) ) )
87 21 85 86 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 )
88 19 87 jca ⊢ ( ( 𝜑 ∧ 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ) → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ∧ 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ) )
89 18 88 mpdan ⊢ ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ∧ 𝐻 ( Circuits ‘ 𝑆 ) 𝑄 ) )