# Metamath Proof Explorer

## Theorem trlsegvdeg

Description: Formerly part of proof of eupth2lem3 : If a trail in a graph G induces a subgraph Z with the vertices V of G and the edges being the edges of the walk, and a subgraph X with the vertices V of G and the edges being the edges of the walk except the last one, and a subgraph Y with the vertices V of G and one edges being the last edge of the walk, then the vertex degree of any vertex U of G within Z is the sum of the vertex degree of U within X and the vertex degree of U within Y . Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
trlsegvdeg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
trlsegvdeg.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
trlsegvdeg.n ${⊢}{\phi }\to {N}\in \left(0..^\left|{F}\right|\right)$
trlsegvdeg.u ${⊢}{\phi }\to {U}\in {V}$
trlsegvdeg.w ${⊢}{\phi }\to {F}\mathrm{Trails}\left({G}\right){P}$
trlsegvdeg.vx ${⊢}{\phi }\to \mathrm{Vtx}\left({X}\right)={V}$
trlsegvdeg.vy ${⊢}{\phi }\to \mathrm{Vtx}\left({Y}\right)={V}$
trlsegvdeg.vz ${⊢}{\phi }\to \mathrm{Vtx}\left({Z}\right)={V}$
trlsegvdeg.ix ${⊢}{\phi }\to \mathrm{iEdg}\left({X}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}$
trlsegvdeg.iy ${⊢}{\phi }\to \mathrm{iEdg}\left({Y}\right)=\left\{⟨{F}\left({N}\right),{I}\left({F}\left({N}\right)\right)⟩\right\}$
trlsegvdeg.iz ${⊢}{\phi }\to \mathrm{iEdg}\left({Z}\right)={{I}↾}_{{F}\left[\left(0\dots {N}\right)\right]}$
Assertion trlsegvdeg ${⊢}{\phi }\to \mathrm{VtxDeg}\left({Z}\right)\left({U}\right)=\mathrm{VtxDeg}\left({X}\right)\left({U}\right)+\mathrm{VtxDeg}\left({Y}\right)\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 trlsegvdeg.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 trlsegvdeg.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 trlsegvdeg.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
4 trlsegvdeg.n ${⊢}{\phi }\to {N}\in \left(0..^\left|{F}\right|\right)$
5 trlsegvdeg.u ${⊢}{\phi }\to {U}\in {V}$
6 trlsegvdeg.w ${⊢}{\phi }\to {F}\mathrm{Trails}\left({G}\right){P}$
7 trlsegvdeg.vx ${⊢}{\phi }\to \mathrm{Vtx}\left({X}\right)={V}$
8 trlsegvdeg.vy ${⊢}{\phi }\to \mathrm{Vtx}\left({Y}\right)={V}$
9 trlsegvdeg.vz ${⊢}{\phi }\to \mathrm{Vtx}\left({Z}\right)={V}$
10 trlsegvdeg.ix ${⊢}{\phi }\to \mathrm{iEdg}\left({X}\right)={{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}$
11 trlsegvdeg.iy ${⊢}{\phi }\to \mathrm{iEdg}\left({Y}\right)=\left\{⟨{F}\left({N}\right),{I}\left({F}\left({N}\right)\right)⟩\right\}$
12 trlsegvdeg.iz ${⊢}{\phi }\to \mathrm{iEdg}\left({Z}\right)={{I}↾}_{{F}\left[\left(0\dots {N}\right)\right]}$
13 eqid ${⊢}\mathrm{iEdg}\left({X}\right)=\mathrm{iEdg}\left({X}\right)$
14 eqid ${⊢}\mathrm{iEdg}\left({Y}\right)=\mathrm{iEdg}\left({Y}\right)$
15 eqid ${⊢}\mathrm{Vtx}\left({X}\right)=\mathrm{Vtx}\left({X}\right)$
16 8 7 eqtr4d ${⊢}{\phi }\to \mathrm{Vtx}\left({Y}\right)=\mathrm{Vtx}\left({X}\right)$
17 9 7 eqtr4d ${⊢}{\phi }\to \mathrm{Vtx}\left({Z}\right)=\mathrm{Vtx}\left({X}\right)$
18 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem4 ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({X}\right)={F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}$
19 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem5 ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({Y}\right)=\left\{{F}\left({N}\right)\right\}$
20 18 19 ineq12d ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({X}\right)\cap \mathrm{dom}\mathrm{iEdg}\left({Y}\right)=\left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)\cap \left\{{F}\left({N}\right)\right\}$
21 fzonel ${⊢}¬{N}\in \left(0..^{N}\right)$
22 2 trlf1 ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}$
23 6 22 syl ${⊢}{\phi }\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}$
24 elfzouz2 ${⊢}{N}\in \left(0..^\left|{F}\right|\right)\to \left|{F}\right|\in {ℤ}_{\ge {N}}$
25 fzoss2 ${⊢}\left|{F}\right|\in {ℤ}_{\ge {N}}\to \left(0..^{N}\right)\subseteq \left(0..^\left|{F}\right|\right)$
26 4 24 25 3syl ${⊢}{\phi }\to \left(0..^{N}\right)\subseteq \left(0..^\left|{F}\right|\right)$
27 f1elima ${⊢}\left({F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}\wedge {N}\in \left(0..^\left|{F}\right|\right)\wedge \left(0..^{N}\right)\subseteq \left(0..^\left|{F}\right|\right)\right)\to \left({F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]↔{N}\in \left(0..^{N}\right)\right)$
28 23 4 26 27 syl3anc ${⊢}{\phi }\to \left({F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]↔{N}\in \left(0..^{N}\right)\right)$
29 21 28 mtbiri ${⊢}{\phi }\to ¬{F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]$
30 29 orcd ${⊢}{\phi }\to \left(¬{F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]\vee ¬{F}\left({N}\right)\in \mathrm{dom}{I}\right)$
31 ianor ${⊢}¬\left({F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]\wedge {F}\left({N}\right)\in \mathrm{dom}{I}\right)↔\left(¬{F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]\vee ¬{F}\left({N}\right)\in \mathrm{dom}{I}\right)$
32 elin ${⊢}{F}\left({N}\right)\in \left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)↔\left({F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]\wedge {F}\left({N}\right)\in \mathrm{dom}{I}\right)$
33 31 32 xchnxbir ${⊢}¬{F}\left({N}\right)\in \left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)↔\left(¬{F}\left({N}\right)\in {F}\left[\left(0..^{N}\right)\right]\vee ¬{F}\left({N}\right)\in \mathrm{dom}{I}\right)$
34 30 33 sylibr ${⊢}{\phi }\to ¬{F}\left({N}\right)\in \left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)$
35 disjsn ${⊢}\left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)\cap \left\{{F}\left({N}\right)\right\}=\varnothing ↔¬{F}\left({N}\right)\in \left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)$
36 34 35 sylibr ${⊢}{\phi }\to \left({F}\left[\left(0..^{N}\right)\right]\cap \mathrm{dom}{I}\right)\cap \left\{{F}\left({N}\right)\right\}=\varnothing$
37 20 36 eqtrd ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({X}\right)\cap \mathrm{dom}\mathrm{iEdg}\left({Y}\right)=\varnothing$
38 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem2 ${⊢}{\phi }\to \mathrm{Fun}\mathrm{iEdg}\left({X}\right)$
39 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem3 ${⊢}{\phi }\to \mathrm{Fun}\mathrm{iEdg}\left({Y}\right)$
40 5 7 eleqtrrd ${⊢}{\phi }\to {U}\in \mathrm{Vtx}\left({X}\right)$
41 f1f ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}{I}\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{I}$
42 6 22 41 3syl ${⊢}{\phi }\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}{I}$
43 3 42 4 resunimafz0 ${⊢}{\phi }\to {{I}↾}_{{F}\left[\left(0\dots {N}\right)\right]}=\left({{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left\{⟨{F}\left({N}\right),{I}\left({F}\left({N}\right)\right)⟩\right\}$
44 10 11 uneq12d ${⊢}{\phi }\to \mathrm{iEdg}\left({X}\right)\cup \mathrm{iEdg}\left({Y}\right)=\left({{I}↾}_{{F}\left[\left(0..^{N}\right)\right]}\right)\cup \left\{⟨{F}\left({N}\right),{I}\left({F}\left({N}\right)\right)⟩\right\}$
45 43 12 44 3eqtr4d ${⊢}{\phi }\to \mathrm{iEdg}\left({Z}\right)=\mathrm{iEdg}\left({X}\right)\cup \mathrm{iEdg}\left({Y}\right)$
46 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem6 ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({X}\right)\in \mathrm{Fin}$
47 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem7 ${⊢}{\phi }\to \mathrm{dom}\mathrm{iEdg}\left({Y}\right)\in \mathrm{Fin}$
48 13 14 15 16 17 37 38 39 40 45 46 47 vtxdfiun ${⊢}{\phi }\to \mathrm{VtxDeg}\left({Z}\right)\left({U}\right)=\mathrm{VtxDeg}\left({X}\right)\left({U}\right)+\mathrm{VtxDeg}\left({Y}\right)\left({U}\right)$