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	\|- ( ph -> F ( EulerPaths ` G ) P )
	eucrct2eupth1.c	\|- ( ph -> F ( Circuits ` G ) P )
	eucrct2eupth1.s	\|- ( Vtx ` S ) = V
	eucrct2eupth1.g	\|- ( ph -> 0 < ( # ` F ) )
	eucrct2eupth1.n	\|- ( ph -> N = ( ( # ` F ) - 1 ) )
	eucrct2eupth1.e	\|- ( ph -> ( iEdg ` S ) = ( I \|` ( F " ( 0 ..^ N ) ) ) )
	eucrct2eupth1.h	\|- H = ( F prefix N )
	eucrct2eupth1.q	\|- Q = ( P \|` ( 0 ... N ) )
Assertion	eucrct2eupth1	\|- ( ph -> H ( EulerPaths ` S ) Q )

Proof

Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	\|- V = ( Vtx ` G )
2		eucrct2eupth1.i	\|- I = ( iEdg ` G )
3		eucrct2eupth1.d	\|- ( ph -> F ( EulerPaths ` G ) P )
4		eucrct2eupth1.c	\|- ( ph -> F ( Circuits ` G ) P )
5		eucrct2eupth1.s	\|- ( Vtx ` S ) = V
6		eucrct2eupth1.g	\|- ( ph -> 0 < ( # ` F ) )
7		eucrct2eupth1.n	\|- ( ph -> N = ( ( # ` F ) - 1 ) )
8		eucrct2eupth1.e	\|- ( ph -> ( iEdg ` S ) = ( I \|` ( F " ( 0 ..^ N ) ) ) )
9		eucrct2eupth1.h	\|- H = ( F prefix N )
10		eucrct2eupth1.q	\|- Q = ( P \|` ( 0 ... N ) )
11		eupthiswlk	\|- ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
12		wlkcl	\|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
13		nn0z	\|- ( ( # ` F ) e. NN0 -> ( # ` F ) e. ZZ )
14	13	anim1i	\|- ( ( ( # ` F ) e. NN0 /\ 0 < ( # ` F ) ) -> ( ( # ` F ) e. ZZ /\ 0 < ( # ` F ) ) )
15		elnnz	\|- ( ( # ` F ) e. NN <-> ( ( # ` F ) e. ZZ /\ 0 < ( # ` F ) ) )
16	14 15	sylibr	\|- ( ( ( # ` F ) e. NN0 /\ 0 < ( # ` F ) ) -> ( # ` F ) e. NN )
17	16	ex	\|- ( ( # ` F ) e. NN0 -> ( 0 < ( # ` F ) -> ( # ` F ) e. NN ) )
18	12 17	syl	\|- ( F ( Walks ` G ) P -> ( 0 < ( # ` F ) -> ( # ` F ) e. NN ) )
19	3 11 18	3syl	\|- ( ph -> ( 0 < ( # ` F ) -> ( # ` F ) e. NN ) )
20	6 19	mpd	\|- ( ph -> ( # ` F ) e. NN )
21		fzo0end	\|- ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
22	20 21	syl	\|- ( ph -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
23	7 22	eqeltrd	\|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
24	1 2 3 23 8 9 10 5	eupthres	\|- ( ph -> H ( EulerPaths ` S ) Q )

Metamath Proof Explorer

Theorem eucrct2eupth1

Proof