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 ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ₀ )
49	9	eleq1i	⊢ ( 𝑁 ∈ ℕ₀ ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ₀ )
50		elnn0uz	⊢ ( 𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ ( ℤ_≥ ‘ 0 ) )
51	49 50	sylbb1	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ₀ → 𝑁 ∈ ( ℤ_≥ ‘ 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 ‘ 𝑆 ) 𝑄 )

Metamath Proof Explorer

Theorem eupthp1

Proof