Theorem eucrct2eupth1

Description: Removing one edge ( I( FN ) ) from a nonempty graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . This is the special case of eucrct2eupth (with J = ( N - 1 ) ) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

	Ref	Expression
Hypotheses	eucrct2eupth1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	eucrct2eupth1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	eucrct2eupth1.d	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
	eucrct2eupth1.c	⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
	eucrct2eupth1.s	⊢ ( Vtx ‘ 𝑆 ) = 𝑉
	eucrct2eupth1.g	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐹 ) )
	eucrct2eupth1.n	⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝐹 ) − 1 ) )
	eucrct2eupth1.e	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
	eucrct2eupth1.h	⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
	eucrct2eupth1.q	⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
Assertion	eucrct2eupth1	⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eucrct2eupth1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		eucrct2eupth1.d	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
4		eucrct2eupth1.c	⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
5		eucrct2eupth1.s	⊢ ( Vtx ‘ 𝑆 ) = 𝑉
6		eucrct2eupth1.g	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐹 ) )
7		eucrct2eupth1.n	⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝐹 ) − 1 ) )
8		eucrct2eupth1.e	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
9		eucrct2eupth1.h	⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
10		eucrct2eupth1.q	⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
11		eupthiswlk	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
12		wlkcl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
13		nn0z	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
14	13	anim1i	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝐹 ) ) )
15		elnnz	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝐹 ) ) )
16	14 15	sylibr	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
17	16	ex	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
18	12 17	syl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 0 < ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
19	3 11 18	3syl	⊢ ( 𝜑 → ( 0 < ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
20	6 19	mpd	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ )
21		fzo0end	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
22	20 21	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
23	7 22	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
24	1 2 3 23 8 9 10 5	eupthres	⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )