Theorem finsumvtxdg2size 29638

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 29639) 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 Σ 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.)

Hypotheses

Ref	Expression
sumvtxdg2size.v	⊢ 𝑉 = (Vtx‘𝐺)
sumvtxdg2size.i	⊢ 𝐼 = (iEdg‘𝐺)
sumvtxdg2size.d	⊢ 𝐷 = (VtxDeg‘𝐺)

Assertion

Ref	Expression
finsumvtxdg2size	⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))

Distinct variable groups:   𝑣,𝐺   𝑣,𝑉

Allowed substitution hints:   𝐷(𝑣)   𝐼(𝑣)

Proof of Theorem finsumvtxdg2size

Dummy variables 𝑒 𝑘 𝑛 𝑓 𝑖 𝑤 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		upgrop 29182	. . . 4 ⊢ (𝐺 ∈ UPGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph)
2		fvex 6841	. . . . . 6 ⊢ (iEdg‘𝐺) ∈ V
3		fvex 6841	. . . . . . 7 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) ∈ V
4	3	resex 5982	. . . . . 6 ⊢ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ V
5		eleq1 2827	. . . . . . . 8 ⊢ (𝑒 = (iEdg‘𝐺) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin))
6	5	adantl 482	. . . . . . 7 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin))
7		simpl 483	. . . . . . . . 9 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → 𝑘 = (Vtx‘𝐺))
8		oveq12 7366	. . . . . . . . . . 11 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑘VtxDeg𝑒) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
9	8	fveq1d 6830	. . . . . . . . . 10 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
10	9	adantr 481	. . . . . . . . 9 ⊢ (((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
11	7, 10	sumeq12dv 15660	. . . . . . . 8 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
12		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑒 = (iEdg‘𝐺) → (♯‘𝑒) = (♯‘(iEdg‘𝐺)))
13	12	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑒 = (iEdg‘𝐺) → (2 · (♯‘𝑒)) = (2 · (♯‘(iEdg‘𝐺))))
14	13	adantl 482	. . . . . . . 8 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (2 · (♯‘𝑒)) = (2 · (♯‘(iEdg‘𝐺))))
15	11, 14	eqeq12d 2755	. . . . . . 7 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
16	6, 15	imbi12d 345	. . . . . 6 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
17		eleq1 2827	. . . . . . . 8 ⊢ (𝑒 = 𝑓 → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin))
18	17	adantl 482	. . . . . . 7 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin))
19		simpl 483	. . . . . . . . 9 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑘 = 𝑤)
20		oveq12 7366	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (𝑤VtxDeg𝑓))
21		df-ov 7360	. . . . . . . . . . . 12 ⊢ (𝑤VtxDeg𝑓) = (VtxDeg‘⟨𝑤, 𝑓⟩)
22	20, 21	eqtrdi 2790	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑤, 𝑓⟩))
23	22	fveq1d 6830	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
24	23	adantr 481	. . . . . . . . 9 ⊢ (((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
25	19, 24	sumeq12dv 15660	. . . . . . . 8 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
26		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑒 = 𝑓 → (♯‘𝑒) = (♯‘𝑓))
27	26	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑒 = 𝑓 → (2 · (♯‘𝑒)) = (2 · (♯‘𝑓)))
28	27	adantl 482	. . . . . . . 8 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (2 · (♯‘𝑒)) = (2 · (♯‘𝑓)))
29	25, 28	eqeq12d 2755	. . . . . . 7 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓))))
30	18, 29	imbi12d 345	. . . . . 6 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ (𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)))))
31		vex 3435	. . . . . . . . 9 ⊢ 𝑘 ∈ V
32		vex 3435	. . . . . . . . 9 ⊢ 𝑒 ∈ V
33	31, 32	opvtxfvi 29097	. . . . . . . 8 ⊢ (Vtx‘⟨𝑘, 𝑒⟩) = 𝑘
34	33	eqcomi 2748	. . . . . . 7 ⊢ 𝑘 = (Vtx‘⟨𝑘, 𝑒⟩)
35		eqid 2739	. . . . . . 7 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) = (iEdg‘⟨𝑘, 𝑒⟩)
36		eqid 2739	. . . . . . 7 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}
37		eqid 2739	. . . . . . 7 ⊢ ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩
38	34, 35, 36, 37	upgrres 29394	. . . . . 6 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) → ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ ∈ UPGraph)
39		eleq1 2827	. . . . . . . 8 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin))
40	39	adantl 482	. . . . . . 7 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin))
41		simpl 483	. . . . . . . . 9 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → 𝑤 = (𝑘 ∖ {𝑛}))
42		opeq12 4807	. . . . . . . . . . . 12 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ⟨𝑤, 𝑓⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)
43	42	fveq2d 6832	. . . . . . . . . . 11 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (VtxDeg‘⟨𝑤, 𝑓⟩) = (VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩))
44	43	fveq1d 6830	. . . . . . . . . 10 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
45	44	adantr 481	. . . . . . . . 9 ⊢ (((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) ∧ 𝑣 ∈ 𝑤) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
46	41, 45	sumeq12dv 15660	. . . . . . . 8 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
47		fveq2 6828	. . . . . . . . . 10 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (♯‘𝑓) = (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))
48	47	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (2 · (♯‘𝑓)) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))
49	48	adantl 482	. . . . . . . 8 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (2 · (♯‘𝑓)) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))
50	46, 49	eqeq12d 2755	. . . . . . 7 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)) ↔ Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))))
51	40, 50	imbi12d 345	. . . . . 6 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ((𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓))) ↔ (((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))))
52		hasheq0 14317	. . . . . . . . 9 ⊢ (𝑘 ∈ V → ((♯‘𝑘) = 0 ↔ 𝑘 = ∅))
53	52	elv 3436	. . . . . . . 8 ⊢ ((♯‘𝑘) = 0 ↔ 𝑘 = ∅)
54		2t0e0 12337	. . . . . . . . . 10 ⊢ (2 · 0) = 0
55	54	a1i 11	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (2 · 0) = 0)
56	31, 32	opiedgfvi 29098	. . . . . . . . . . . . 13 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) = 𝑒
57	56	eqcomi 2748	. . . . . . . . . . . 12 ⊢ 𝑒 = (iEdg‘⟨𝑘, 𝑒⟩)
58		upgruhgr 29190	. . . . . . . . . . . . . 14 ⊢ (⟨𝑘, 𝑒⟩ ∈ UPGraph → ⟨𝑘, 𝑒⟩ ∈ UHGraph)
59	58	adantr 481	. . . . . . . . . . . . 13 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → ⟨𝑘, 𝑒⟩ ∈ UHGraph)
60	34	eqeq1i 2744	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ∅ ↔ (Vtx‘⟨𝑘, 𝑒⟩) = ∅)
61		uhgr0vb 29160	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (Vtx‘⟨𝑘, 𝑒⟩) = ∅) → (⟨𝑘, 𝑒⟩ ∈ UHGraph ↔ (iEdg‘⟨𝑘, 𝑒⟩) = ∅))
62	60, 61	sylan2b 600	. . . . . . . . . . . . 13 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (⟨𝑘, 𝑒⟩ ∈ UHGraph ↔ (iEdg‘⟨𝑘, 𝑒⟩) = ∅))
63	59, 62	mpbid 233	. . . . . . . . . . . 12 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (iEdg‘⟨𝑘, 𝑒⟩) = ∅)
64	57, 63	eqtrid 2786	. . . . . . . . . . 11 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → 𝑒 = ∅)
65		hasheq0 14317	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ V → ((♯‘𝑒) = 0 ↔ 𝑒 = ∅))
66	65	elv 3436	. . . . . . . . . . 11 ⊢ ((♯‘𝑒) = 0 ↔ 𝑒 = ∅)
67	64, 66	sylibr 235	. . . . . . . . . 10 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (♯‘𝑒) = 0)
68	67	oveq2d 7373	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (2 · (♯‘𝑒)) = (2 · 0))
69		sumeq1 15643	. . . . . . . . . . 11 ⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣))
70		sum0 15675	. . . . . . . . . . 11 ⊢ Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣) = 0
71	69, 70	eqtrdi 2790	. . . . . . . . . 10 ⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0)
72	71	adantl 482	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0)
73	55, 68, 72	3eqtr4rd 2785	. . . . . . . 8 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))
74	53, 73	sylan2b 600	. . . . . . 7 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = 0) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))
75	74	a1d 25	. . . . . 6 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = 0) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))
76		eleq1 2827	. . . . . . . . . . 11 ⊢ ((𝑦 + 1) = (♯‘𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
77	76	eqcoms 2747	. . . . . . . . . 10 ⊢ ((♯‘𝑘) = (𝑦 + 1) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
78	77	3ad2ant2 1140	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
79		hashclb 14312	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ V → (𝑘 ∈ Fin ↔ (♯‘𝑘) ∈ ℕ0))
80	79	biimprd 249	. . . . . . . . . . 11 ⊢ (𝑘 ∈ V → ((♯‘𝑘) ∈ ℕ0 → 𝑘 ∈ Fin))
81	80	elv 3436	. . . . . . . . . 10 ⊢ ((♯‘𝑘) ∈ ℕ0 → 𝑘 ∈ Fin)
82		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∖ {𝑛}) = (𝑘 ∖ {𝑛})
83		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
84	56	dmeqi 5847	. . . . . . . . . . . . . . . . . 18 ⊢ dom (iEdg‘⟨𝑘, 𝑒⟩) = dom 𝑒
85	84	rabeqi 3404	. . . . . . . . . . . . . . . . 17 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}
86		eqidd 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ dom 𝑒 → 𝑛 = 𝑛)
87	56	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ dom 𝑒 → (iEdg‘⟨𝑘, 𝑒⟩) = 𝑒)
88	87	fveq1d 6830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ dom 𝑒 → ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) = (𝑒‘𝑖))
89	86, 88	neleq12d 3043	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ dom 𝑒 → (𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) ↔ 𝑛 ∉ (𝑒‘𝑖)))
90	89	rabbiia 3395	. . . . . . . . . . . . . . . . 17 ⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
91	85, 90	eqtri 2762	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
92	56, 91	reseq12i 5930	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) = (𝑒 ↾ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)})
93	34, 57, 82, 83, 92, 37	finsumvtxdg2sstep 29637	. . . . . . . . . . . . . 14 ⊢ (((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒))))
94		df-ov 7360	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑘, 𝑒⟩)
95	94	fveq1i 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣)
96	95	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑘 → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣))
97	96	sumeq2i 15652	. . . . . . . . . . . . . . 15 ⊢ Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣)
98	97	eqeq1i 2744	. . . . . . . . . . . . . 14 ⊢ (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒)))
99	93, 98	imbitrrdi 253	. . . . . . . . . . . . 13 ⊢ (((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))
100	99	exp32 421	. . . . . . . . . . . 12 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → (𝑒 ∈ Fin → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))))
101	100	com34 91	. . . . . . . . . . 11 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))))
102	101	3adant2 1137	. . . . . . . . . 10 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → (𝑘 ∈ Fin → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))))
103	81, 102	syl5 34	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((♯‘𝑘) ∈ ℕ0 → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))))
104	78, 103	sylbid 241	. . . . . . . 8 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))))
105	104	impcom 408	. . . . . . 7 ⊢ (((𝑦 + 1) ∈ ℕ0 ∧ (⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘)) → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))))
106	105	imp 407	. . . . . 6 ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘)) ∧ (((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))
107	2, 4, 16, 30, 38, 51, 75, 106	opfi1ind 14466	. . . . 5 ⊢ ((⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph ∧ (Vtx‘𝐺) ∈ Fin) → ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
108	107	ex 413	. . . 4 ⊢ (⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph → ((Vtx‘𝐺) ∈ Fin → ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
109	1, 108	syl 17	. . 3 ⊢ (𝐺 ∈ UPGraph → ((Vtx‘𝐺) ∈ Fin → ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
110		sumvtxdg2size.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
111	110	eleq1i 2830	. . . 4 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
112	111	a1i 11	. . 3 ⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin))
113		sumvtxdg2size.i	. . . . . 6 ⊢ 𝐼 = (iEdg‘𝐺)
114	113	eleq1i 2830	. . . . 5 ⊢ (𝐼 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)
115	114	a1i 11	. . . 4 ⊢ (𝐺 ∈ UPGraph → (𝐼 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin))
116	110	a1i 11	. . . . . 6 ⊢ (𝐺 ∈ UPGraph → 𝑉 = (Vtx‘𝐺))
117		sumvtxdg2size.d	. . . . . . . . 9 ⊢ 𝐷 = (VtxDeg‘𝐺)
118		vtxdgop 29558	. . . . . . . . 9 ⊢ (𝐺 ∈ UPGraph → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
119	117, 118	eqtrid 2786	. . . . . . . 8 ⊢ (𝐺 ∈ UPGraph → 𝐷 = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
120	119	fveq1d 6830	. . . . . . 7 ⊢ (𝐺 ∈ UPGraph → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
121	120	adantr 481	. . . . . 6 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑣 ∈ 𝑉) → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
122	116, 121	sumeq12dv 15660	. . . . 5 ⊢ (𝐺 ∈ UPGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
123	113	fveq2i 6831	. . . . . . 7 ⊢ (♯‘𝐼) = (♯‘(iEdg‘𝐺))
124	123	oveq2i 7368	. . . . . 6 ⊢ (2 · (♯‘𝐼)) = (2 · (♯‘(iEdg‘𝐺)))
125	124	a1i 11	. . . . 5 ⊢ (𝐺 ∈ UPGraph → (2 · (♯‘𝐼)) = (2 · (♯‘(iEdg‘𝐺))))
126	122, 125	eqeq12d 2755	. . . 4 ⊢ (𝐺 ∈ UPGraph → (Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
127	115, 126	imbi12d 345	. . 3 ⊢ (𝐺 ∈ UPGraph → ((𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
128	109, 112, 127	3imtr4d 295	. 2 ⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin → (𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))))
129	128	3imp 1116	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ∉ wnel 3038  {crab 3391  Vcvv 3431   ∖ cdif 3880  ∅c0 4262  {csn 4556  ⟨cop 4562  dom cdm 5619   ↾ cres 5621  ‘cfv 6486  (class class class)co 7357  Fincfn 8884  0cc0 11030  1c1 11031   + caddc 11033   · cmul 11035  2c2 12228  ℕ₀cn0 12429  ♯chash 14284  Σcsu 15640  Vtxcvtx 29084  iEdgciedg 29085  UHGraphcuhgr 29144  UPGraphcupgr 29168  VtxDegcvtxdg 29553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5200  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-inf2 9554  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107  ax-pre-sup 11108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-int 4879  df-iun 4924  df-disj 5041  df-br 5074  df-opab 5136  df-mpt 5155  df-tr 5181  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7314  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7808  df-1st 7932  df-2nd 7933  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-1o 8396  df-2o 8397  df-oadd 8400  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9346  df-oi 9416  df-dju 9817  df-card 9855  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177  df-sub 11371  df-neg 11372  df-div 11800  df-nn 12167  df-2 12236  df-3 12237  df-n0 12430  df-xnn0 12503  df-z 12517  df-uz 12781  df-rp 12935  df-xadd 13056  df-fz 13454  df-fzo 13601  df-seq 13956  df-exp 14016  df-hash 14285  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-clim 15442  df-sum 15641  df-vtx 29086  df-iedg 29087  df-edg 29136  df-uhgr 29146  df-upgr 29170  df-vtxdg 29554

This theorem is referenced by:  fusgr1th  29639  finsumvtxdgeven  29640