# Metamath Proof Explorer

## Theorem finsumvtxdg2size

Description: The sum of the degrees of all vertices of a finite pseudograph of finite size is twice the size of the pseudograph. See equation (1) in section I.1 in Bollobas p. 4. Here, the "proof" is simply the statement "Since each edge has two endvertices, the sum of the degrees is exactly twice the number of edges". The formal proof of this theorem (for pseudographs) is much more complicated, taking also the used auxiliary theorems into account. The proof for a (finite) simple graph (see fusgr1th ) would be shorter, but nevertheless still laborious. Although this theorem would hold also for infinite pseudographs and pseudographs of infinite size, the proof of this most general version (see theorem "sumvtxdg2size" below) would require many more auxiliary theorems (e.g., the extension of the sum sum_ over an arbitrary set).

I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021)

Ref Expression
Hypotheses sumvtxdg2size.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
sumvtxdg2size.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
sumvtxdg2size.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
Assertion finsumvtxdg2size ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {V}\in \mathrm{Fin}\wedge {I}\in \mathrm{Fin}\right)\to \sum _{{v}\in {V}}{D}\left({v}\right)=2\left|{I}\right|$

### Proof

Step Hyp Ref Expression
1 sumvtxdg2size.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 sumvtxdg2size.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 sumvtxdg2size.d ${⊢}{D}=\mathrm{VtxDeg}\left({G}\right)$
4 upgrop ${⊢}{G}\in \mathrm{UPGraph}\to ⟨\mathrm{Vtx}\left({G}\right),\mathrm{iEdg}\left({G}\right)⟩\in \mathrm{UPGraph}$
5 fvex ${⊢}\mathrm{iEdg}\left({G}\right)\in \mathrm{V}$
6 fvex ${⊢}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)\in \mathrm{V}$
7 6 resex ${⊢}{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{V}$
8 eleq1 ${⊢}{e}=\mathrm{iEdg}\left({G}\right)\to \left({e}\in \mathrm{Fin}↔\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\right)$
9 8 adantl ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to \left({e}\in \mathrm{Fin}↔\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\right)$
10 simpl ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to {k}=\mathrm{Vtx}\left({G}\right)$
11 oveq12 ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to {k}\mathrm{VtxDeg}{e}=\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)$
12 11 fveq1d ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to \left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
13 12 adantr ${⊢}\left(\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\wedge {v}\in {k}\right)\to \left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
14 10 13 sumeq12dv ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
15 fveq2 ${⊢}{e}=\mathrm{iEdg}\left({G}\right)\to \left|{e}\right|=\left|\mathrm{iEdg}\left({G}\right)\right|$
16 15 oveq2d ${⊢}{e}=\mathrm{iEdg}\left({G}\right)\to 2\left|{e}\right|=2\left|\mathrm{iEdg}\left({G}\right)\right|$
17 16 adantl ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to 2\left|{e}\right|=2\left|\mathrm{iEdg}\left({G}\right)\right|$
18 14 17 eqeq12d ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to \left(\sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|↔\sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)$
19 9 18 imbi12d ${⊢}\left({k}=\mathrm{Vtx}\left({G}\right)\wedge {e}=\mathrm{iEdg}\left({G}\right)\right)\to \left(\left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)↔\left(\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\to \sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)\right)$
20 eleq1 ${⊢}{e}={f}\to \left({e}\in \mathrm{Fin}↔{f}\in \mathrm{Fin}\right)$
21 20 adantl ${⊢}\left({k}={w}\wedge {e}={f}\right)\to \left({e}\in \mathrm{Fin}↔{f}\in \mathrm{Fin}\right)$
22 simpl ${⊢}\left({k}={w}\wedge {e}={f}\right)\to {k}={w}$
23 oveq12 ${⊢}\left({k}={w}\wedge {e}={f}\right)\to {k}\mathrm{VtxDeg}{e}={w}\mathrm{VtxDeg}{f}$
24 df-ov ${⊢}{w}\mathrm{VtxDeg}{f}=\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)$
25 23 24 syl6eq ${⊢}\left({k}={w}\wedge {e}={f}\right)\to {k}\mathrm{VtxDeg}{e}=\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)$
26 25 fveq1d ${⊢}\left({k}={w}\wedge {e}={f}\right)\to \left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)$
27 26 adantr ${⊢}\left(\left({k}={w}\wedge {e}={f}\right)\wedge {v}\in {k}\right)\to \left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)$
28 22 27 sumeq12dv ${⊢}\left({k}={w}\wedge {e}={f}\right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)$
29 fveq2 ${⊢}{e}={f}\to \left|{e}\right|=\left|{f}\right|$
30 29 oveq2d ${⊢}{e}={f}\to 2\left|{e}\right|=2\left|{f}\right|$
31 30 adantl ${⊢}\left({k}={w}\wedge {e}={f}\right)\to 2\left|{e}\right|=2\left|{f}\right|$
32 28 31 eqeq12d ${⊢}\left({k}={w}\wedge {e}={f}\right)\to \left(\sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|↔\sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=2\left|{f}\right|\right)$
33 21 32 imbi12d ${⊢}\left({k}={w}\wedge {e}={f}\right)\to \left(\left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)↔\left({f}\in \mathrm{Fin}\to \sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=2\left|{f}\right|\right)\right)$
34 vex ${⊢}{k}\in \mathrm{V}$
35 vex ${⊢}{e}\in \mathrm{V}$
36 34 35 opvtxfvi ${⊢}\mathrm{Vtx}\left(⟨{k},{e}⟩\right)={k}$
37 36 eqcomi ${⊢}{k}=\mathrm{Vtx}\left(⟨{k},{e}⟩\right)$
38 eqid ${⊢}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)=\mathrm{iEdg}\left(⟨{k},{e}⟩\right)$
39 eqid ${⊢}\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}=\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}$
40 eqid ${⊢}⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩=⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩$
41 37 38 39 40 upgrres ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {n}\in {k}\right)\to ⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\in \mathrm{UPGraph}$
42 eleq1 ${⊢}{f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\to \left({f}\in \mathrm{Fin}↔{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\right)$
43 42 adantl ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \left({f}\in \mathrm{Fin}↔{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\right)$
44 simpl ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to {w}={k}\setminus \left\{{n}\right\}$
45 opeq12 ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to ⟨{w},{f}⟩=⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩$
46 45 fveq2d ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)=\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)$
47 46 fveq1d ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)$
48 47 adantr ${⊢}\left(\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\wedge {v}\in {w}\right)\to \mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)$
49 44 48 sumeq12dv ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=\sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)$
50 fveq2 ${⊢}{f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\to \left|{f}\right|=\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|$
51 50 oveq2d ${⊢}{f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\to 2\left|{f}\right|=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|$
52 51 adantl ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to 2\left|{f}\right|=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|$
53 49 52 eqeq12d ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \left(\sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=2\left|{f}\right|↔\sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)$
54 43 53 imbi12d ${⊢}\left({w}={k}\setminus \left\{{n}\right\}\wedge {f}={\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right)\to \left(\left({f}\in \mathrm{Fin}\to \sum _{{v}\in {w}}\mathrm{VtxDeg}\left(⟨{w},{f}⟩\right)\left({v}\right)=2\left|{f}\right|\right)↔\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\right)$
55 hasheq0 ${⊢}{k}\in \mathrm{V}\to \left(\left|{k}\right|=0↔{k}=\varnothing \right)$
56 55 elv ${⊢}\left|{k}\right|=0↔{k}=\varnothing$
57 2t0e0 ${⊢}2\cdot 0=0$
58 57 a1i ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to 2\cdot 0=0$
59 34 35 opiedgfvi ${⊢}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)={e}$
60 59 eqcomi ${⊢}{e}=\mathrm{iEdg}\left(⟨{k},{e}⟩\right)$
61 upgruhgr ${⊢}⟨{k},{e}⟩\in \mathrm{UPGraph}\to ⟨{k},{e}⟩\in \mathrm{UHGraph}$
62 61 adantr ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to ⟨{k},{e}⟩\in \mathrm{UHGraph}$
63 37 eqeq1i ${⊢}{k}=\varnothing ↔\mathrm{Vtx}\left(⟨{k},{e}⟩\right)=\varnothing$
64 uhgr0vb ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \mathrm{Vtx}\left(⟨{k},{e}⟩\right)=\varnothing \right)\to \left(⟨{k},{e}⟩\in \mathrm{UHGraph}↔\mathrm{iEdg}\left(⟨{k},{e}⟩\right)=\varnothing \right)$
65 63 64 sylan2b ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to \left(⟨{k},{e}⟩\in \mathrm{UHGraph}↔\mathrm{iEdg}\left(⟨{k},{e}⟩\right)=\varnothing \right)$
66 62 65 mpbid ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to \mathrm{iEdg}\left(⟨{k},{e}⟩\right)=\varnothing$
67 60 66 syl5eq ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to {e}=\varnothing$
68 hasheq0 ${⊢}{e}\in \mathrm{V}\to \left(\left|{e}\right|=0↔{e}=\varnothing \right)$
69 68 elv ${⊢}\left|{e}\right|=0↔{e}=\varnothing$
70 67 69 sylibr ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to \left|{e}\right|=0$
71 70 oveq2d ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to 2\left|{e}\right|=2\cdot 0$
72 sumeq1 ${⊢}{k}=\varnothing \to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\sum _{{v}\in \varnothing }\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)$
73 sum0 ${⊢}\sum _{{v}\in \varnothing }\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=0$
74 72 73 syl6eq ${⊢}{k}=\varnothing \to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=0$
75 74 adantl ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=0$
76 58 71 75 3eqtr4rd ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {k}=\varnothing \right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|$
77 56 76 sylan2b ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|=0\right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|$
78 77 a1d ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|=0\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)$
79 eleq1 ${⊢}{y}+1=\left|{k}\right|\to \left({y}+1\in {ℕ}_{0}↔\left|{k}\right|\in {ℕ}_{0}\right)$
80 79 eqcoms ${⊢}\left|{k}\right|={y}+1\to \left({y}+1\in {ℕ}_{0}↔\left|{k}\right|\in {ℕ}_{0}\right)$
81 80 3ad2ant2 ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\to \left({y}+1\in {ℕ}_{0}↔\left|{k}\right|\in {ℕ}_{0}\right)$
82 hashclb ${⊢}{k}\in \mathrm{V}\to \left({k}\in \mathrm{Fin}↔\left|{k}\right|\in {ℕ}_{0}\right)$
83 82 biimprd ${⊢}{k}\in \mathrm{V}\to \left(\left|{k}\right|\in {ℕ}_{0}\to {k}\in \mathrm{Fin}\right)$
84 83 elv ${⊢}\left|{k}\right|\in {ℕ}_{0}\to {k}\in \mathrm{Fin}$
85 eqid ${⊢}{k}\setminus \left\{{n}\right\}={k}\setminus \left\{{n}\right\}$
86 eqid ${⊢}\left\{{i}\in \mathrm{dom}{e}|{n}\notin {e}\left({i}\right)\right\}=\left\{{i}\in \mathrm{dom}{e}|{n}\notin {e}\left({i}\right)\right\}$
87 59 dmeqi ${⊢}\mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)=\mathrm{dom}{e}$
88 87 rabeqi ${⊢}\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}=\left\{{i}\in \mathrm{dom}{e}|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}$
89 eqidd ${⊢}{i}\in \mathrm{dom}{e}\to {n}={n}$
90 59 a1i ${⊢}{i}\in \mathrm{dom}{e}\to \mathrm{iEdg}\left(⟨{k},{e}⟩\right)={e}$
91 90 fveq1d ${⊢}{i}\in \mathrm{dom}{e}\to \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)={e}\left({i}\right)$
92 89 91 neleq12d ${⊢}{i}\in \mathrm{dom}{e}\to \left({n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)↔{n}\notin {e}\left({i}\right)\right)$
93 92 rabbiia ${⊢}\left\{{i}\in \mathrm{dom}{e}|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}=\left\{{i}\in \mathrm{dom}{e}|{n}\notin {e}\left({i}\right)\right\}$
94 88 93 eqtri ${⊢}\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}=\left\{{i}\in \mathrm{dom}{e}|{n}\notin {e}\left({i}\right)\right\}$
95 59 94 reseq12i ${⊢}{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}={{e}↾}_{\left\{{i}\in \mathrm{dom}{e}|{n}\notin {e}\left({i}\right)\right\}}$
96 37 60 85 86 95 40 finsumvtxdg2sstep ${⊢}\left(\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {n}\in {k}\right)\wedge \left({k}\in \mathrm{Fin}\wedge {e}\in \mathrm{Fin}\right)\right)\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \sum _{{v}\in {k}}\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)\left({v}\right)=2\left|{e}\right|\right)$
97 df-ov ${⊢}{k}\mathrm{VtxDeg}{e}=\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)$
98 97 fveq1i ${⊢}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)\left({v}\right)$
99 98 a1i ${⊢}{v}\in {k}\to \left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)\left({v}\right)$
100 99 sumeq2i ${⊢}\sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=\sum _{{v}\in {k}}\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)\left({v}\right)$
101 100 eqeq1i ${⊢}\sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|↔\sum _{{v}\in {k}}\mathrm{VtxDeg}\left(⟨{k},{e}⟩\right)\left({v}\right)=2\left|{e}\right|$
102 96 101 syl6ibr ${⊢}\left(\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {n}\in {k}\right)\wedge \left({k}\in \mathrm{Fin}\wedge {e}\in \mathrm{Fin}\right)\right)\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)$
103 102 exp32 ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {n}\in {k}\right)\to \left({k}\in \mathrm{Fin}\to \left({e}\in \mathrm{Fin}\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)\right)$
104 103 com34 ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge {n}\in {k}\right)\to \left({k}\in \mathrm{Fin}\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)\right)$
105 104 3adant2 ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\to \left({k}\in \mathrm{Fin}\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)\right)$
106 84 105 syl5 ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\to \left(\left|{k}\right|\in {ℕ}_{0}\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)\right)$
107 81 106 sylbid ${⊢}\left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\to \left({y}+1\in {ℕ}_{0}\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)\right)$
108 107 impcom ${⊢}\left({y}+1\in {ℕ}_{0}\wedge \left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\right)\to \left(\left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)\right)$
109 108 imp ${⊢}\left(\left({y}+1\in {ℕ}_{0}\wedge \left(⟨{k},{e}⟩\in \mathrm{UPGraph}\wedge \left|{k}\right|={y}+1\wedge {n}\in {k}\right)\right)\wedge \left({\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\in \mathrm{Fin}\to \sum _{{v}\in {k}\setminus \left\{{n}\right\}}\mathrm{VtxDeg}\left(⟨{k}\setminus \left\{{n}\right\},{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}⟩\right)\left({v}\right)=2\left|{\mathrm{iEdg}\left(⟨{k},{e}⟩\right)↾}_{\left\{{i}\in \mathrm{dom}\mathrm{iEdg}\left(⟨{k},{e}⟩\right)|{n}\notin \mathrm{iEdg}\left(⟨{k},{e}⟩\right)\left({i}\right)\right\}}\right|\right)\right)\to \left({e}\in \mathrm{Fin}\to \sum _{{v}\in {k}}\left({k}\mathrm{VtxDeg}{e}\right)\left({v}\right)=2\left|{e}\right|\right)$
110 5 7 19 33 41 54 78 109 opfi1ind ${⊢}\left(⟨\mathrm{Vtx}\left({G}\right),\mathrm{iEdg}\left({G}\right)⟩\in \mathrm{UPGraph}\wedge \mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}\right)\to \left(\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\to \sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)$
111 110 ex ${⊢}⟨\mathrm{Vtx}\left({G}\right),\mathrm{iEdg}\left({G}\right)⟩\in \mathrm{UPGraph}\to \left(\mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}\to \left(\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\to \sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)\right)$
112 4 111 syl ${⊢}{G}\in \mathrm{UPGraph}\to \left(\mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}\to \left(\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\to \sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)\right)$
113 1 eleq1i ${⊢}{V}\in \mathrm{Fin}↔\mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}$
114 113 a1i ${⊢}{G}\in \mathrm{UPGraph}\to \left({V}\in \mathrm{Fin}↔\mathrm{Vtx}\left({G}\right)\in \mathrm{Fin}\right)$
115 2 eleq1i ${⊢}{I}\in \mathrm{Fin}↔\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}$
116 115 a1i ${⊢}{G}\in \mathrm{UPGraph}\to \left({I}\in \mathrm{Fin}↔\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\right)$
117 1 a1i ${⊢}{G}\in \mathrm{UPGraph}\to {V}=\mathrm{Vtx}\left({G}\right)$
118 vtxdgop ${⊢}{G}\in \mathrm{UPGraph}\to \mathrm{VtxDeg}\left({G}\right)=\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)$
119 3 118 syl5eq ${⊢}{G}\in \mathrm{UPGraph}\to {D}=\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)$
120 119 fveq1d ${⊢}{G}\in \mathrm{UPGraph}\to {D}\left({v}\right)=\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
121 120 adantr ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {v}\in {V}\right)\to {D}\left({v}\right)=\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
122 117 121 sumeq12dv ${⊢}{G}\in \mathrm{UPGraph}\to \sum _{{v}\in {V}}{D}\left({v}\right)=\sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)$
123 2 fveq2i ${⊢}\left|{I}\right|=\left|\mathrm{iEdg}\left({G}\right)\right|$
124 123 oveq2i ${⊢}2\left|{I}\right|=2\left|\mathrm{iEdg}\left({G}\right)\right|$
125 124 a1i ${⊢}{G}\in \mathrm{UPGraph}\to 2\left|{I}\right|=2\left|\mathrm{iEdg}\left({G}\right)\right|$
126 122 125 eqeq12d ${⊢}{G}\in \mathrm{UPGraph}\to \left(\sum _{{v}\in {V}}{D}\left({v}\right)=2\left|{I}\right|↔\sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)$
127 116 126 imbi12d ${⊢}{G}\in \mathrm{UPGraph}\to \left(\left({I}\in \mathrm{Fin}\to \sum _{{v}\in {V}}{D}\left({v}\right)=2\left|{I}\right|\right)↔\left(\mathrm{iEdg}\left({G}\right)\in \mathrm{Fin}\to \sum _{{v}\in \mathrm{Vtx}\left({G}\right)}\left(\mathrm{Vtx}\left({G}\right)\mathrm{VtxDeg}\mathrm{iEdg}\left({G}\right)\right)\left({v}\right)=2\left|\mathrm{iEdg}\left({G}\right)\right|\right)\right)$
128 112 114 127 3imtr4d ${⊢}{G}\in \mathrm{UPGraph}\to \left({V}\in \mathrm{Fin}\to \left({I}\in \mathrm{Fin}\to \sum _{{v}\in {V}}{D}\left({v}\right)=2\left|{I}\right|\right)\right)$
129 128 3imp ${⊢}\left({G}\in \mathrm{UPGraph}\wedge {V}\in \mathrm{Fin}\wedge {I}\in \mathrm{Fin}\right)\to \sum _{{v}\in {V}}{D}\left({v}\right)=2\left|{I}\right|$