eupth2lem3

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	eupth2.v	\|- V = ( Vtx ` G )
	eupth2.i	\|- I = ( iEdg ` G )
	eupth2.g	\|- ( ph -> G e. UPGraph )
	eupth2.f	\|- ( ph -> Fun I )
	eupth2.p	\|- ( ph -> F ( EulerPaths ` G ) P )
	eupth2.h	\|- H = <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >.
	eupth2.x	\|- X = <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >.
	eupth2.n	\|- ( ph -> N e. NN0 )
	eupth2.l	\|- ( ph -> ( N + 1 ) <_ ( # ` F ) )
	eupth2.u	\|- ( ph -> U e. V )
	eupth2.o	\|- ( ph -> { x e. V \| -. 2 \|\| ( ( VtxDeg ` H ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
Assertion	eupth2lem3	\|- ( ph -> ( -. 2 \|\| ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	\|- V = ( Vtx ` G )
2		eupth2.i	\|- I = ( iEdg ` G )
3		eupth2.g	\|- ( ph -> G e. UPGraph )
4		eupth2.f	\|- ( ph -> Fun I )
5		eupth2.p	\|- ( ph -> F ( EulerPaths ` G ) P )
6		eupth2.h	\|- H = <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >.
7		eupth2.x	\|- X = <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >.
8		eupth2.n	\|- ( ph -> N e. NN0 )
9		eupth2.l	\|- ( ph -> ( N + 1 ) <_ ( # ` F ) )
10		eupth2.u	\|- ( ph -> U e. V )
11		eupth2.o	\|- ( ph -> { x e. V \| -. 2 \|\| ( ( VtxDeg ` H ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
12		eupthiswlk	\|- ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
13		wlkcl	\|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
14	5 12 13	3syl	\|- ( ph -> ( # ` F ) e. NN0 )
15		nn0p1elfzo	\|- ( ( N e. NN0 /\ ( # ` F ) e. NN0 /\ ( N + 1 ) <_ ( # ` F ) ) -> N e. ( 0 ..^ ( # ` F ) ) )
16	8 14 9 15	syl3anc	\|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
17		eupthistrl	\|- ( F ( EulerPaths ` G ) P -> F ( Trails ` G ) P )
18	5 17	syl	\|- ( ph -> F ( Trails ` G ) P )
19	6	fveq2i	\|- ( Vtx ` H ) = ( Vtx ` <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >. )
20	1	fvexi	\|- V e. _V
21	2	fvexi	\|- I e. _V
22	21	resex	\|- ( I \|` ( F " ( 0 ..^ N ) ) ) e. _V
23	20 22	opvtxfvi	\|- ( Vtx ` <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >. ) = V
24	19 23	eqtri	\|- ( Vtx ` H ) = V
25	24	a1i	\|- ( ph -> ( Vtx ` H ) = V )
26		snex	\|- { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } e. _V
27	20 26	opvtxfvi	\|- ( Vtx ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = V
28	27	a1i	\|- ( ph -> ( Vtx ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = V )
29	7	fveq2i	\|- ( Vtx ` X ) = ( Vtx ` <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. )
30	21	resex	\|- ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) e. _V
31	20 30	opvtxfvi	\|- ( Vtx ` <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. ) = V
32	29 31	eqtri	\|- ( Vtx ` X ) = V
33	32	a1i	\|- ( ph -> ( Vtx ` X ) = V )
34	6	fveq2i	\|- ( iEdg ` H ) = ( iEdg ` <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >. )
35	20 22	opiedgfvi	\|- ( iEdg ` <. V , ( I \|` ( F " ( 0 ..^ N ) ) ) >. ) = ( I \|` ( F " ( 0 ..^ N ) ) )
36	34 35	eqtri	\|- ( iEdg ` H ) = ( I \|` ( F " ( 0 ..^ N ) ) )
37	36	a1i	\|- ( ph -> ( iEdg ` H ) = ( I \|` ( F " ( 0 ..^ N ) ) ) )
38	20 26	opiedgfvi	\|- ( iEdg ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. }
39	38	a1i	\|- ( ph -> ( iEdg ` <. V , { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } >. ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
40	7	fveq2i	\|- ( iEdg ` X ) = ( iEdg ` <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. )
41	20 30	opiedgfvi	\|- ( iEdg ` <. V , ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) >. ) = ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) )
42	40 41	eqtri	\|- ( iEdg ` X ) = ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) )
43	8	nn0zd	\|- ( ph -> N e. ZZ )
44		fzval3	\|- ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
45	44	eqcomd	\|- ( N e. ZZ -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
46	43 45	syl	\|- ( ph -> ( 0 ..^ ( N + 1 ) ) = ( 0 ... N ) )
47	46	imaeq2d	\|- ( ph -> ( F " ( 0 ..^ ( N + 1 ) ) ) = ( F " ( 0 ... N ) ) )
48	47	reseq2d	\|- ( ph -> ( I \|` ( F " ( 0 ..^ ( N + 1 ) ) ) ) = ( I \|` ( F " ( 0 ... N ) ) ) )
49	42 48	syl5eq	\|- ( ph -> ( iEdg ` X ) = ( I \|` ( F " ( 0 ... N ) ) ) )
50		2fveq3	\|- ( k = N -> ( I ` ( F ` k ) ) = ( I ` ( F ` N ) ) )
51		fveq2	\|- ( k = N -> ( P ` k ) = ( P ` N ) )
52		fvoveq1	\|- ( k = N -> ( P ` ( k + 1 ) ) = ( P ` ( N + 1 ) ) )
53	51 52	preq12d	\|- ( k = N -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
54	50 53	eqeq12d	\|- ( k = N -> ( ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
55	5 12	syl	\|- ( ph -> F ( Walks ` G ) P )
56	2	upgrwlkedg	\|- ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
57	3 55 56	syl2anc	\|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
58	54 57 16	rspcdva	\|- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
59	1 2 4 16 10 18 25 28 33 37 39 49 11 58	eupth2lem3lem7	\|- ( ph -> ( -. 2 \|\| ( ( VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Metamath Proof Explorer

Theorem eupth2lem3

Proof