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