Metamath Proof Explorer

Theorem eupthp1

Description: Append one path segment to an Eulerian path <. F , P >. to become an Eulerian path <. H , Q >. of the supergraph S obtained by adding the new edge to the graph G . (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 7-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 ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑃 ‘ 𝑁 ) ) → 𝐸 = { 𝐶 } )
Assertion eupthp1 ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

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 eupthiswlk ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
18 8 17 syl ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
19 12 a1i ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
20 15 a1i ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
21 1 2 3 4 5 6 7 18 9 10 11 19 13 14 20 16 wlkp1 ⊢ ( 𝜑 → 𝐻 ( Walks ‘ 𝑆 ) 𝑄 )
22 2 eupthi ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) )
23 9 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
24 23 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 )
25 f1oeq2 ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 𝑁 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 ) )
26 24 25 ax-mp ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 )
27 26 biimpi ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 → 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 )
28 27 adantl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) → 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 )
29 8 22 28 3syl ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 )
30 9 fvexi ⊢ 𝑁 ∈ V
31 f1osng ⊢ ( ( 𝑁 ∈ V ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ { 𝐵 } )
32 30 5 31 sylancr ⊢ ( 𝜑 → { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ { 𝐵 } )
33 dmsnopg ⊢ ( 𝐸 ∈ ( Edg ‘ 𝐺 ) → dom { ⟨ 𝐵 , 𝐸 ⟩ } = { 𝐵 } )
34 10 33 syl ⊢ ( 𝜑 → dom { ⟨ 𝐵 , 𝐸 ⟩ } = { 𝐵 } )
35 34 f1oeq3d ⊢ ( 𝜑 → ( { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ dom { ⟨ 𝐵 , 𝐸 ⟩ } ↔ { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ { 𝐵 } ) )
36 32 35 mpbird ⊢ ( 𝜑 → { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ dom { ⟨ 𝐵 , 𝐸 ⟩ } )
37 fzodisjsn ⊢ ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅
38 37 a1i ⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ )
39 34 ineq2d ⊢ ( 𝜑 → ( dom 𝐼 ∩ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) = ( dom 𝐼 ∩ { 𝐵 } ) )
40 disjsn ⊢ ( ( dom 𝐼 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ dom 𝐼 )
41 7 40 sylibr ⊢ ( 𝜑 → ( dom 𝐼 ∩ { 𝐵 } ) = ∅ )
42 39 41 eqtrd ⊢ ( 𝜑 → ( dom 𝐼 ∩ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) = ∅ )
43 f1oun ⊢ ( ( ( 𝐹 : ( 0 ..^ 𝑁 ) –1-1-onto→ dom 𝐼 ∧ { ⟨ 𝑁 , 𝐵 ⟩ } : { 𝑁 } –1-1-onto→ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) ∧ ( ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ ∧ ( dom 𝐼 ∩ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) = ∅ ) ) → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) –1-1-onto→ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
44 29 36 38 42 43 syl22anc ⊢ ( 𝜑 → ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) –1-1-onto→ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
45 13 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
46 1 2 3 4 5 6 7 18 9 10 11 19 13 wlkp1lem2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )
47 46 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
48 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
49 9 eleq1i ⊢ ( 𝑁 ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
50 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
51 49 50 sylbb1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
52 48 51 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
53 8 17 52 3syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
54 fzosplitsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
55 53 54 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
56 47 55 eqtrd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐻 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
57 dmun ⊢ dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) = ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } )
58 57 a1i ⊢ ( 𝜑 → dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) = ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) )
59 45 56 58 f1oeq123d ⊢ ( 𝜑 → ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ↔ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) : ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) –1-1-onto→ ( dom 𝐼 ∪ dom { ⟨ 𝐵 , 𝐸 ⟩ } ) ) )
60 44 59 mpbird ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
61 12 eqcomi ⊢ ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) = ( iEdg ‘ 𝑆 )
62 61 iseupthf1o ⊢ ( 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 ↔ ( 𝐻 ( Walks ‘ 𝑆 ) 𝑄 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) –1-1-onto→ dom ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ) )
63 21 60 62 sylanbrc ⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )