This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
sumvtxdg2size.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
sumvtxdg2size.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion finsumvtxdg2size ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )

Proof

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