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 = Vtx (G)$
	sumvtxdg2size.i	$⊢ I = iEdg (G)$
	sumvtxdg2size.d	$⊢ D = VtxDeg (G)$
Assertion	finsumvtxdg2size	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \sum_{v \in V} D (v) = 2 \|I\|$

Proof

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

Metamath Proof Explorer

Theorem finsumvtxdg2size

Proof