Theorem eupth2lem3

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

	Ref	Expression
Hypotheses	eupth2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	eupth2.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	eupth2.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
	eupth2.f	$$⊢\phi \to \mathrm{Fun}I$$
	eupth2.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
	eupth2.h	$$⊢H=⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩$$
	eupth2.x	$$⊢X=⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩$$
	eupth2.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	eupth2.l	$$⊢\phi \to N+1\le \left|F\right|$$
	eupth2.u	$$⊢\phi \to U\in V$$
	eupth2.o	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(H\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(N\right),\varnothing ,\left\{P\left(0\right),P\left(N\right)\right\}\right)$$
Assertion	eupth2lem3	$$⊢\phi \to \left(\neg 2\parallel \mathrm{VtxDeg}\left(X\right)\left(U\right)\leftrightarrow U\in if\left(P\left(0\right)=P\left(N+1\right),\varnothing ,\left\{P\left(0\right),P\left(N+1\right)\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		eupth2.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		eupth2.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
4		eupth2.f	$$⊢\phi \to \mathrm{Fun}I$$
5		eupth2.p	$$⊢\phi \to F\mathrm{EulerPaths}\left(G\right)P$$
6		eupth2.h	$$⊢H=⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩$$
7		eupth2.x	$$⊢X=⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩$$
8		eupth2.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		eupth2.l	$$⊢\phi \to N+1\le \left|F\right|$$
10		eupth2.u	$$⊢\phi \to U\in V$$
11		eupth2.o	$$⊢\phi \to \left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(H\right)\left(x\right)\right\}=if\left(P\left(0\right)=P\left(N\right),\varnothing ,\left\{P\left(0\right),P\left(N\right)\right\}\right)$$
12		eupthiswlk	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Walks}\left(G\right)P$$
13		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
14	5 12 13	3syl	$$⊢\phi \to \left|F\right|\in {\mathbb{N}}_0$$
15		nn0p1elfzo	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left|F\right|\in {\mathbb{N}}_0\wedge N+1\le \left|F\right|\right)\to N\in \left(0..^\left|F\right|\right)$$
16	8 14 9 15	syl3anc	$$⊢\phi \to N\in \left(0..^\left|F\right|\right)$$
17		eupthistrl	$$⊢F\mathrm{EulerPaths}\left(G\right)P\to F\mathrm{Trails}\left(G\right)P$$
18	5 17	syl	$$⊢\phi \to F\mathrm{Trails}\left(G\right)P$$
19	6	fveq2i	$$⊢\mathrm{Vtx}\left(H\right)=\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩\right)$$
20	1	fvexi	$$⊢V\in \mathrm{V}$$
21	2	fvexi	$$⊢I\in \mathrm{V}$$
22	21	resex	$$⊢{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}\in \mathrm{V}$$
23	20 22	opvtxfvi	$$⊢\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩\right)=V$$
24	19 23	eqtri	$$⊢\mathrm{Vtx}\left(H\right)=V$$
25	24	a1i	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
26		snex	$$⊢\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}\in \mathrm{V}$$
27	20 26	opvtxfvi	$$⊢\mathrm{Vtx}\left(⟨V,\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}⟩\right)=V$$
28	27	a1i	$$⊢\phi \to \mathrm{Vtx}\left(⟨V,\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}⟩\right)=V$$
29	7	fveq2i	$$⊢\mathrm{Vtx}\left(X\right)=\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩\right)$$
30	21	resex	$$⊢{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}\in \mathrm{V}$$
31	20 30	opvtxfvi	$$⊢\mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩\right)=V$$
32	29 31	eqtri	$$⊢\mathrm{Vtx}\left(X\right)=V$$
33	32	a1i	$$⊢\phi \to \mathrm{Vtx}\left(X\right)=V$$
34	6	fveq2i	$$⊢\mathrm{iEdg}\left(H\right)=\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩\right)$$
35	20 22	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
36	34 35	eqtri	$$⊢\mathrm{iEdg}\left(H\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
37	36	a1i	$$⊢\phi \to \mathrm{iEdg}\left(H\right)={I\upharpoonright }_{F\left[\left(0..^N\right)\right]}$$
38	20 26	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨V,\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}⟩\right)=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
39	38	a1i	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}⟩\right)=\left\{⟨F\left(N\right),I\left(F\left(N\right)\right)⟩\right\}$$
40	7	fveq2i	$$⊢\mathrm{iEdg}\left(X\right)=\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩\right)$$
41	20 30	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}$$
42	40 41	eqtri	$$⊢\mathrm{iEdg}\left(X\right)={I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}$$
43	8	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
44		fzval3	$$⊢N\in \mathbb{Z}\to \left(0\dots N\right)=\left(0..^N+1\right)$$
45	44	eqcomd	$$⊢N\in \mathbb{Z}\to \left(0..^N+1\right)=\left(0\dots N\right)$$
46	43 45	syl	$$⊢\phi \to \left(0..^N+1\right)=\left(0\dots N\right)$$
47	46	imaeq2d	$$⊢\phi \to F\left[\left(0..^N+1\right)\right]=F\left[\left(0\dots N\right)\right]$$
48	47	reseq2d	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0..^N+1\right)\right]}={I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}$$
49	42 48	eqtrid	$$⊢\phi \to \mathrm{iEdg}\left(X\right)={I\upharpoonright }_{F\left[\left(0\dots N\right)\right]}$$
50		2fveq3	$$⊢k=N\to I\left(F\left(k\right)\right)=I\left(F\left(N\right)\right)$$
51		fveq2	$$⊢k=N\to P\left(k\right)=P\left(N\right)$$
52		fvoveq1	$$⊢k=N\to P\left(k+1\right)=P\left(N+1\right)$$
53	51 52	preq12d	$$⊢k=N\to \left\{P\left(k\right),P\left(k+1\right)\right\}=\left\{P\left(N\right),P\left(N+1\right)\right\}$$
54	50 53	eqeq12d	$$⊢k=N\to \left(I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}\leftrightarrow I\left(F\left(N\right)\right)=\left\{P\left(N\right),P\left(N+1\right)\right\}\right)$$
55	5 12	syl	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
56	2	upgrwlkedg	$$⊢\left(G\in \mathrm{UPGraph}\wedge F\mathrm{Walks}\left(G\right)P\right)\to \forall k\in \left(0..^\left|F\right|\right)I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$
57	3 55 56	syl2anc	$$⊢\phi \to \forall k\in \left(0..^\left|F\right|\right)I\left(F\left(k\right)\right)=\left\{P\left(k\right),P\left(k+1\right)\right\}$$
58	54 57 16	rspcdva	$$⊢\phi \to I\left(F\left(N\right)\right)=\left\{P\left(N\right),P\left(N+1\right)\right\}$$
59	1 2 4 16 10 18 25 28 33 37 39 49 11 58	eupth2lem3lem7	$$⊢\phi \to \left(\neg 2\parallel \mathrm{VtxDeg}\left(X\right)\left(U\right)\leftrightarrow U\in if\left(P\left(0\right)=P\left(N+1\right),\varnothing ,\left\{P\left(0\right),P\left(N+1\right)\right\}\right)\right)$$