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=VtxG
sumvtxdg2size.i I=iEdgG
sumvtxdg2size.d D=VtxDegG
Assertion finsumvtxdg2size GUPGraphVFinIFinvVDv=2I

Proof

Step Hyp Ref Expression
1 sumvtxdg2size.v V=VtxG
2 sumvtxdg2size.i I=iEdgG
3 sumvtxdg2size.d D=VtxDegG
4 upgrop GUPGraphVtxGiEdgGUPGraph
5 fvex iEdgGV
6 fvex iEdgkeV
7 6 resex iEdgkeidomiEdgke|niEdgkeiV
8 eleq1 e=iEdgGeFiniEdgGFin
9 8 adantl k=VtxGe=iEdgGeFiniEdgGFin
10 simpl k=VtxGe=iEdgGk=VtxG
11 oveq12 k=VtxGe=iEdgGkVtxDege=VtxGVtxDegiEdgG
12 11 fveq1d k=VtxGe=iEdgGkVtxDegev=VtxGVtxDegiEdgGv
13 12 adantr k=VtxGe=iEdgGvkkVtxDegev=VtxGVtxDegiEdgGv
14 10 13 sumeq12dv k=VtxGe=iEdgGvkkVtxDegev=vVtxGVtxGVtxDegiEdgGv
15 fveq2 e=iEdgGe=iEdgG
16 15 oveq2d e=iEdgG2e=2iEdgG
17 16 adantl k=VtxGe=iEdgG2e=2iEdgG
18 14 17 eqeq12d k=VtxGe=iEdgGvkkVtxDegev=2evVtxGVtxGVtxDegiEdgGv=2iEdgG
19 9 18 imbi12d k=VtxGe=iEdgGeFinvkkVtxDegev=2eiEdgGFinvVtxGVtxGVtxDegiEdgGv=2iEdgG
20 eleq1 e=feFinfFin
21 20 adantl k=we=feFinfFin
22 simpl k=we=fk=w
23 oveq12 k=we=fkVtxDege=wVtxDegf
24 df-ov wVtxDegf=VtxDegwf
25 23 24 eqtrdi k=we=fkVtxDege=VtxDegwf
26 25 fveq1d k=we=fkVtxDegev=VtxDegwfv
27 26 adantr k=we=fvkkVtxDegev=VtxDegwfv
28 22 27 sumeq12dv k=we=fvkkVtxDegev=vwVtxDegwfv
29 fveq2 e=fe=f
30 29 oveq2d e=f2e=2f
31 30 adantl k=we=f2e=2f
32 28 31 eqeq12d k=we=fvkkVtxDegev=2evwVtxDegwfv=2f
33 21 32 imbi12d k=we=feFinvkkVtxDegev=2efFinvwVtxDegwfv=2f
34 vex kV
35 vex eV
36 34 35 opvtxfvi Vtxke=k
37 36 eqcomi k=Vtxke
38 eqid iEdgke=iEdgke
39 eqid idomiEdgke|niEdgkei=idomiEdgke|niEdgkei
40 eqid kniEdgkeidomiEdgke|niEdgkei=kniEdgkeidomiEdgke|niEdgkei
41 37 38 39 40 upgrres keUPGraphnkkniEdgkeidomiEdgke|niEdgkeiUPGraph
42 eleq1 f=iEdgkeidomiEdgke|niEdgkeifFiniEdgkeidomiEdgke|niEdgkeiFin
43 42 adantl w=knf=iEdgkeidomiEdgke|niEdgkeifFiniEdgkeidomiEdgke|niEdgkeiFin
44 simpl w=knf=iEdgkeidomiEdgke|niEdgkeiw=kn
45 opeq12 w=knf=iEdgkeidomiEdgke|niEdgkeiwf=kniEdgkeidomiEdgke|niEdgkei
46 45 fveq2d w=knf=iEdgkeidomiEdgke|niEdgkeiVtxDegwf=VtxDegkniEdgkeidomiEdgke|niEdgkei
47 46 fveq1d w=knf=iEdgkeidomiEdgke|niEdgkeiVtxDegwfv=VtxDegkniEdgkeidomiEdgke|niEdgkeiv
48 47 adantr w=knf=iEdgkeidomiEdgke|niEdgkeivwVtxDegwfv=VtxDegkniEdgkeidomiEdgke|niEdgkeiv
49 44 48 sumeq12dv w=knf=iEdgkeidomiEdgke|niEdgkeivwVtxDegwfv=vknVtxDegkniEdgkeidomiEdgke|niEdgkeiv
50 fveq2 f=iEdgkeidomiEdgke|niEdgkeif=iEdgkeidomiEdgke|niEdgkei
51 50 oveq2d f=iEdgkeidomiEdgke|niEdgkei2f=2iEdgkeidomiEdgke|niEdgkei
52 51 adantl w=knf=iEdgkeidomiEdgke|niEdgkei2f=2iEdgkeidomiEdgke|niEdgkei
53 49 52 eqeq12d w=knf=iEdgkeidomiEdgke|niEdgkeivwVtxDegwfv=2fvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkei
54 43 53 imbi12d w=knf=iEdgkeidomiEdgke|niEdgkeifFinvwVtxDegwfv=2fiEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkei
55 hasheq0 kVk=0k=
56 55 elv k=0k=
57 2t0e0 20=0
58 57 a1i keUPGraphk=20=0
59 34 35 opiedgfvi iEdgke=e
60 59 eqcomi e=iEdgke
61 upgruhgr keUPGraphkeUHGraph
62 61 adantr keUPGraphk=keUHGraph
63 37 eqeq1i k=Vtxke=
64 uhgr0vb keUPGraphVtxke=keUHGraphiEdgke=
65 63 64 sylan2b keUPGraphk=keUHGraphiEdgke=
66 62 65 mpbid keUPGraphk=iEdgke=
67 60 66 eqtrid keUPGraphk=e=
68 hasheq0 eVe=0e=
69 68 elv e=0e=
70 67 69 sylibr keUPGraphk=e=0
71 70 oveq2d keUPGraphk=2e=20
72 sumeq1 k=vkkVtxDegev=vkVtxDegev
73 sum0 vkVtxDegev=0
74 72 73 eqtrdi k=vkkVtxDegev=0
75 74 adantl keUPGraphk=vkkVtxDegev=0
76 58 71 75 3eqtr4rd keUPGraphk=vkkVtxDegev=2e
77 56 76 sylan2b keUPGraphk=0vkkVtxDegev=2e
78 77 a1d keUPGraphk=0eFinvkkVtxDegev=2e
79 eleq1 y+1=ky+10k0
80 79 eqcoms k=y+1y+10k0
81 80 3ad2ant2 keUPGraphk=y+1nky+10k0
82 hashclb kVkFink0
83 82 biimprd kVk0kFin
84 83 elv k0kFin
85 eqid kn=kn
86 eqid idome|nei=idome|nei
87 59 dmeqi domiEdgke=dome
88 87 rabeqi idomiEdgke|niEdgkei=idome|niEdgkei
89 eqidd idomen=n
90 59 a1i idomeiEdgke=e
91 90 fveq1d idomeiEdgkei=ei
92 89 91 neleq12d idomeniEdgkeinei
93 92 rabbiia idome|niEdgkei=idome|nei
94 88 93 eqtri idomiEdgke|niEdgkei=idome|nei
95 59 94 reseq12i iEdgkeidomiEdgke|niEdgkei=eidome|nei
96 37 60 85 86 95 40 finsumvtxdg2sstep keUPGraphnkkFineFiniEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeivkVtxDegkev=2e
97 df-ov kVtxDege=VtxDegke
98 97 fveq1i kVtxDegev=VtxDegkev
99 98 a1i vkkVtxDegev=VtxDegkev
100 99 sumeq2i vkkVtxDegev=vkVtxDegkev
101 100 eqeq1i vkkVtxDegev=2evkVtxDegkev=2e
102 96 101 syl6ibr keUPGraphnkkFineFiniEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeivkkVtxDegev=2e
103 102 exp32 keUPGraphnkkFineFiniEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeivkkVtxDegev=2e
104 103 com34 keUPGraphnkkFiniEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
105 104 3adant2 keUPGraphk=y+1nkkFiniEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
106 84 105 syl5 keUPGraphk=y+1nkk0iEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
107 81 106 sylbid keUPGraphk=y+1nky+10iEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
108 107 impcom y+10keUPGraphk=y+1nkiEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
109 108 imp y+10keUPGraphk=y+1nkiEdgkeidomiEdgke|niEdgkeiFinvknVtxDegkniEdgkeidomiEdgke|niEdgkeiv=2iEdgkeidomiEdgke|niEdgkeieFinvkkVtxDegev=2e
110 5 7 19 33 41 54 78 109 opfi1ind VtxGiEdgGUPGraphVtxGFiniEdgGFinvVtxGVtxGVtxDegiEdgGv=2iEdgG
111 110 ex VtxGiEdgGUPGraphVtxGFiniEdgGFinvVtxGVtxGVtxDegiEdgGv=2iEdgG
112 4 111 syl GUPGraphVtxGFiniEdgGFinvVtxGVtxGVtxDegiEdgGv=2iEdgG
113 1 eleq1i VFinVtxGFin
114 113 a1i GUPGraphVFinVtxGFin
115 2 eleq1i IFiniEdgGFin
116 115 a1i GUPGraphIFiniEdgGFin
117 1 a1i GUPGraphV=VtxG
118 vtxdgop GUPGraphVtxDegG=VtxGVtxDegiEdgG
119 3 118 eqtrid GUPGraphD=VtxGVtxDegiEdgG
120 119 fveq1d GUPGraphDv=VtxGVtxDegiEdgGv
121 120 adantr GUPGraphvVDv=VtxGVtxDegiEdgGv
122 117 121 sumeq12dv GUPGraphvVDv=vVtxGVtxGVtxDegiEdgGv
123 2 fveq2i I=iEdgG
124 123 oveq2i 2I=2iEdgG
125 124 a1i GUPGraph2I=2iEdgG
126 122 125 eqeq12d GUPGraphvVDv=2IvVtxGVtxGVtxDegiEdgGv=2iEdgG
127 116 126 imbi12d GUPGraphIFinvVDv=2IiEdgGFinvVtxGVtxGVtxDegiEdgGv=2iEdgG
128 112 114 127 3imtr4d GUPGraphVFinIFinvVDv=2I
129 128 3imp GUPGraphVFinIFinvVDv=2I