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