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 ‘ 𝑆 ) 𝑄 ) )