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	$⊢ V = Vtx (G)$
	eucrct2eupth1.i	$⊢ I = iEdg (G)$
	eucrct2eupth1.d	$⊢ φ \to F EulerPaths (G) P$
	eucrct2eupth1.c	$⊢ φ \to F Circuits (G) P$
	eucrct2eupth1.s	$⊢ Vtx (S) = V$
	eucrct2eupth1.g	$⊢ φ \to 0 < \|F\|$
	eucrct2eupth1.n	$⊢ φ \to N = \|F\| - 1$
	eucrct2eupth1.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N)]}$
	eucrct2eupth1.h	$⊢ H = F prefix N$
	eucrct2eupth1.q	$⊢ Q = {P ↾}_{(0 \dots N)}$
Assertion	eucrct2eupth1	$⊢ φ \to H EulerPaths (S) Q$

Proof

Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	$⊢ V = Vtx (G)$
2		eucrct2eupth1.i	$⊢ I = iEdg (G)$
3		eucrct2eupth1.d	$⊢ φ \to F EulerPaths (G) P$
4		eucrct2eupth1.c	$⊢ φ \to F Circuits (G) P$
5		eucrct2eupth1.s	$⊢ Vtx (S) = V$
6		eucrct2eupth1.g	$⊢ φ \to 0 < \|F\|$
7		eucrct2eupth1.n	$⊢ φ \to N = \|F\| - 1$
8		eucrct2eupth1.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N)]}$
9		eucrct2eupth1.h	$⊢ H = F prefix N$
10		eucrct2eupth1.q	$⊢ Q = {P ↾}_{(0 \dots N)}$
11		eupthiswlk	$⊢ F EulerPaths (G) P \to F Walks (G) P$
12		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
13		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
14	13	anim1i	$⊢ (\|F\| \in ℕ_{0} \land 0 < \|F\|) \to (\|F\| \in ℤ \land 0 < \|F\|)$
15		elnnz	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℤ \land 0 < \|F\|)$
16	14 15	sylibr	$⊢ (\|F\| \in ℕ_{0} \land 0 < \|F\|) \to \|F\| \in ℕ$
17	16	ex	$⊢ \|F\| \in ℕ_{0} \to (0 < \|F\| \to \|F\| \in ℕ)$
18	3 11 12 17	4syl	$⊢ φ \to (0 < \|F\| \to \|F\| \in ℕ)$
19	6 18	mpd	$⊢ φ \to \|F\| \in ℕ$
20		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
21	19 20	syl	$⊢ φ \to \|F\| - 1 \in (0 ..^\|F\|)$
22	7 21	eqeltrd	$⊢ φ \to N \in (0 ..^\|F\|)$
23	1 2 3 22 8 9 10 5	eupthres	$⊢ φ \to H EulerPaths (S) Q$

Metamath Proof Explorer

Theorem eucrct2eupth1

Proof