# Metamath Proof Explorer

## 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}↾}_{{F}\left[\left(0..^{N}\right)\right]}⟩$
eupth2.x ${⊢}{X}=⟨{V},{{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}⟩$
eupth2.n ${⊢}{\phi }\to {N}\in {ℕ}_{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}|¬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(¬2\parallel \mathrm{VtxDeg}\left({X}\right)\left({U}\right)↔{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}↾}_{{F}\left[\left(0..^{N}\right)\right]}⟩$
7 eupth2.x ${⊢}{X}=⟨{V},{{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}⟩$
8 eupth2.n ${⊢}{\phi }\to {N}\in {ℕ}_{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}|¬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 {ℕ}_{0}$
14 5 12 13 3syl ${⊢}{\phi }\to \left|{F}\right|\in {ℕ}_{0}$
15 nn0p1elfzo ${⊢}\left({N}\in {ℕ}_{0}\wedge \left|{F}\right|\in {ℕ}_{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}↾}_{{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}↾}_{{F}\left[\left(0..^{N}\right)\right]}\in \mathrm{V}$
23 20 22 opvtxfvi ${⊢}\mathrm{Vtx}\left(⟨{V},{{I}↾}_{{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}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}⟩\right)$
30 21 resex ${⊢}{{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}\in \mathrm{V}$
31 20 30 opvtxfvi ${⊢}\mathrm{Vtx}\left(⟨{V},{{I}↾}_{{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}↾}_{{F}\left[\left(0..^{N}\right)\right]}⟩\right)$
35 20 22 opiedgfvi ${⊢}\mathrm{iEdg}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}⟩\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}$
36 34 35 eqtri ${⊢}\mathrm{iEdg}\left({H}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}$
37 36 a1i ${⊢}{\phi }\to \mathrm{iEdg}\left({H}\right)={{I}↾}_{{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}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}⟩\right)$
41 20 30 opiedgfvi ${⊢}\mathrm{iEdg}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}⟩\right)={{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}$
42 40 41 eqtri ${⊢}\mathrm{iEdg}\left({X}\right)={{I}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}$
43 8 nn0zd ${⊢}{\phi }\to {N}\in ℤ$
44 fzval3 ${⊢}{N}\in ℤ\to \left(0\dots {N}\right)=\left(0..^{N}+1\right)$
45 44 eqcomd ${⊢}{N}\in ℤ\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}↾}_{{F}\left[\left(0..^{N}+1\right)\right]}={{I}↾}_{{F}\left[\left(0\dots {N}\right)\right]}$
49 42 48 syl5eq ${⊢}{\phi }\to \mathrm{iEdg}\left({X}\right)={{I}↾}_{{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\}↔{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)\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{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(¬2\parallel \mathrm{VtxDeg}\left({X}\right)\left({U}\right)↔{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)$