Theorem finsumvtxdg2size 29529

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 29530) 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 29072	. . . 4 ⊢ (𝐺 ∈ UPGraph → ⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph)
2		fvex 6916	. . . . . 6 ⊢ (iEdg‘𝐺) ∈ V
3		fvex 6916	. . . . . . 7 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) ∈ V
4	3	resex 6041	. . . . . 6 ⊢ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ V
5		eleq1 2817	. . . . . . . 8 ⊢ (𝑒 = (iEdg‘𝐺) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin))
6	5	adantl 480	. . . . . . 7 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin))
7		simpl 481	. . . . . . . . 9 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → 𝑘 = (Vtx‘𝐺))
8		oveq12 7436	. . . . . . . . . . 11 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑘VtxDeg𝑒) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
9	8	fveq1d 6905	. . . . . . . . . 10 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
10	9	adantr 479	. . . . . . . . 9 ⊢ (((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
11	7, 10	sumeq12dv 15723	. . . . . . . 8 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
12		fveq2 6903	. . . . . . . . . 10 ⊢ (𝑒 = (iEdg‘𝐺) → (♯‘𝑒) = (♯‘(iEdg‘𝐺)))
13	12	oveq2d 7443	. . . . . . . . 9 ⊢ (𝑒 = (iEdg‘𝐺) → (2 · (♯‘𝑒)) = (2 · (♯‘(iEdg‘𝐺))))
14	13	adantl 480	. . . . . . . 8 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (2 · (♯‘𝑒)) = (2 · (♯‘(iEdg‘𝐺))))
15	11, 14	eqeq12d 2745	. . . . . . 7 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
16	6, 15	imbi12d 343	. . . . . 6 ⊢ ((𝑘 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
17		eleq1 2817	. . . . . . . 8 ⊢ (𝑒 = 𝑓 → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin))
18	17	adantl 480	. . . . . . 7 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin))
19		simpl 481	. . . . . . . . 9 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → 𝑘 = 𝑤)
20		oveq12 7436	. . . . . . . . . . . 12 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (𝑤VtxDeg𝑓))
21		df-ov 7430	. . . . . . . . . . . 12 ⊢ (𝑤VtxDeg𝑓) = (VtxDeg‘⟨𝑤, 𝑓⟩)
22	20, 21	eqtrdi 2785	. . . . . . . . . . 11 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑤, 𝑓⟩))
23	22	fveq1d 6905	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
24	23	adantr 479	. . . . . . . . 9 ⊢ (((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) ∧ 𝑣 ∈ 𝑘) → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
25	19, 24	sumeq12dv 15723	. . . . . . . 8 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣))
26		fveq2 6903	. . . . . . . . . 10 ⊢ (𝑒 = 𝑓 → (♯‘𝑒) = (♯‘𝑓))
27	26	oveq2d 7443	. . . . . . . . 9 ⊢ (𝑒 = 𝑓 → (2 · (♯‘𝑒)) = (2 · (♯‘𝑓)))
28	27	adantl 480	. . . . . . . 8 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (2 · (♯‘𝑒)) = (2 · (♯‘𝑓)))
29	25, 28	eqeq12d 2745	. . . . . . 7 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓))))
30	18, 29	imbi12d 343	. . . . . 6 ⊢ ((𝑘 = 𝑤 ∧ 𝑒 = 𝑓) → ((𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))) ↔ (𝑓 ∈ Fin → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)))))
31		vex 3476	. . . . . . . . 9 ⊢ 𝑘 ∈ V
32		vex 3476	. . . . . . . . 9 ⊢ 𝑒 ∈ V
33	31, 32	opvtxfvi 28987	. . . . . . . 8 ⊢ (Vtx‘⟨𝑘, 𝑒⟩) = 𝑘
34	33	eqcomi 2738	. . . . . . 7 ⊢ 𝑘 = (Vtx‘⟨𝑘, 𝑒⟩)
35		eqid 2729	. . . . . . 7 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) = (iEdg‘⟨𝑘, 𝑒⟩)
36		eqid 2729	. . . . . . 7 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}
37		eqid 2729	. . . . . . 7 ⊢ ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩
38	34, 35, 36, 37	upgrres 29284	. . . . . 6 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) → ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩ ∈ UPGraph)
39		eleq1 2817	. . . . . . . 8 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin))
40	39	adantl 480	. . . . . . 7 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (𝑓 ∈ Fin ↔ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin))
41		simpl 481	. . . . . . . . 9 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → 𝑤 = (𝑘 ∖ {𝑛}))
42		opeq12 4884	. . . . . . . . . . . 12 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ⟨𝑤, 𝑓⟩ = ⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)
43	42	fveq2d 6907	. . . . . . . . . . 11 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (VtxDeg‘⟨𝑤, 𝑓⟩) = (VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩))
44	43	fveq1d 6905	. . . . . . . . . 10 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
45	44	adantr 479	. . . . . . . . 9 ⊢ (((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) ∧ 𝑣 ∈ 𝑤) → ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = ((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
46	41, 45	sumeq12dv 15723	. . . . . . . 8 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣))
47		fveq2 6903	. . . . . . . . . 10 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (♯‘𝑓) = (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))
48	47	oveq2d 7443	. . . . . . . . 9 ⊢ (𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) → (2 · (♯‘𝑓)) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))
49	48	adantl 480	. . . . . . . 8 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (2 · (♯‘𝑓)) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}))))
50	46, 49	eqeq12d 2745	. . . . . . 7 ⊢ ((𝑤 = (𝑘 ∖ {𝑛}) ∧ 𝑓 = ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})) → (Σ𝑣 ∈ 𝑤 ((VtxDeg‘⟨𝑤, 𝑓⟩)‘𝑣) = (2 · (♯‘𝑓)) ↔ Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))))
51	40, 50	imbi12d 343	. . . . . 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 14386	. . . . . . . . 9 ⊢ (𝑘 ∈ V → ((♯‘𝑘) = 0 ↔ 𝑘 = ∅))
53	52	elv 3478	. . . . . . . 8 ⊢ ((♯‘𝑘) = 0 ↔ 𝑘 = ∅)
54		2t0e0 12437	. . . . . . . . . 10 ⊢ (2 · 0) = 0
55	54	a1i 11	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (2 · 0) = 0)
56	31, 32	opiedgfvi 28988	. . . . . . . . . . . . 13 ⊢ (iEdg‘⟨𝑘, 𝑒⟩) = 𝑒
57	56	eqcomi 2738	. . . . . . . . . . . 12 ⊢ 𝑒 = (iEdg‘⟨𝑘, 𝑒⟩)
58		upgruhgr 29080	. . . . . . . . . . . . . 14 ⊢ (⟨𝑘, 𝑒⟩ ∈ UPGraph → ⟨𝑘, 𝑒⟩ ∈ UHGraph)
59	58	adantr 479	. . . . . . . . . . . . 13 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → ⟨𝑘, 𝑒⟩ ∈ UHGraph)
60	34	eqeq1i 2734	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ∅ ↔ (Vtx‘⟨𝑘, 𝑒⟩) = ∅)
61		uhgr0vb 29050	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (Vtx‘⟨𝑘, 𝑒⟩) = ∅) → (⟨𝑘, 𝑒⟩ ∈ UHGraph ↔ (iEdg‘⟨𝑘, 𝑒⟩) = ∅))
62	60, 61	sylan2b 592	. . . . . . . . . . . . 13 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (⟨𝑘, 𝑒⟩ ∈ UHGraph ↔ (iEdg‘⟨𝑘, 𝑒⟩) = ∅))
63	59, 62	mpbid 231	. . . . . . . . . . . 12 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (iEdg‘⟨𝑘, 𝑒⟩) = ∅)
64	57, 63	eqtrid 2781	. . . . . . . . . . 11 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → 𝑒 = ∅)
65		hasheq0 14386	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ V → ((♯‘𝑒) = 0 ↔ 𝑒 = ∅))
66	65	elv 3478	. . . . . . . . . . 11 ⊢ ((♯‘𝑒) = 0 ↔ 𝑒 = ∅)
67	64, 66	sylibr 233	. . . . . . . . . 10 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (♯‘𝑒) = 0)
68	67	oveq2d 7443	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → (2 · (♯‘𝑒)) = (2 · 0))
69		sumeq1 15706	. . . . . . . . . . 11 ⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣))
70		sum0 15738	. . . . . . . . . . 11 ⊢ Σ𝑣 ∈ ∅ ((𝑘VtxDeg𝑒)‘𝑣) = 0
71	69, 70	eqtrdi 2785	. . . . . . . . . 10 ⊢ (𝑘 = ∅ → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0)
72	71	adantl 480	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = 0)
73	55, 68, 72	3eqtr4rd 2780	. . . . . . . 8 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑘 = ∅) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))
74	53, 73	sylan2b 592	. . . . . . 7 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = 0) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)))
75	74	a1d 25	. . . . . 6 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = 0) → (𝑒 ∈ Fin → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))
76		eleq1 2817	. . . . . . . . . . 11 ⊢ ((𝑦 + 1) = (♯‘𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
77	76	eqcoms 2737	. . . . . . . . . 10 ⊢ ((♯‘𝑘) = (𝑦 + 1) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
78	77	3ad2ant2 1131	. . . . . . . . 9 ⊢ ((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ (♯‘𝑘) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑘) → ((𝑦 + 1) ∈ ℕ0 ↔ (♯‘𝑘) ∈ ℕ0))
79		hashclb 14381	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ V → (𝑘 ∈ Fin ↔ (♯‘𝑘) ∈ ℕ0))
80	79	biimprd 247	. . . . . . . . . . 11 ⊢ (𝑘 ∈ V → ((♯‘𝑘) ∈ ℕ0 → 𝑘 ∈ Fin))
81	80	elv 3478	. . . . . . . . . 10 ⊢ ((♯‘𝑘) ∈ ℕ0 → 𝑘 ∈ Fin)
82		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∖ {𝑛}) = (𝑘 ∖ {𝑛})
83		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
84	56	dmeqi 5913	. . . . . . . . . . . . . . . . . 18 ⊢ dom (iEdg‘⟨𝑘, 𝑒⟩) = dom 𝑒
85	84	rabeqi 3442	. . . . . . . . . . . . . . . . 17 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}
86		eqidd 2730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ dom 𝑒 → 𝑛 = 𝑛)
87	56	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ dom 𝑒 → (iEdg‘⟨𝑘, 𝑒⟩) = 𝑒)
88	87	fveq1d 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ dom 𝑒 → ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) = (𝑒‘𝑖))
89	86, 88	neleq12d 3044	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ dom 𝑒 → (𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖) ↔ 𝑛 ∉ (𝑒‘𝑖)))
90	89	rabbiia 3432	. . . . . . . . . . . . . . . . 17 ⊢ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
91	85, 90	eqtri 2757	. . . . . . . . . . . . . . . 16 ⊢ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)} = {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)}
92	56, 91	reseq12i 5990	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) = (𝑒 ↾ {𝑖 ∈ dom 𝑒 ∣ 𝑛 ∉ (𝑒‘𝑖)})
93	34, 57, 82, 83, 92, 37	finsumvtxdg2sstep 29528	. . . . . . . . . . . . . 14 ⊢ (((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒))))
94		df-ov 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘VtxDeg𝑒) = (VtxDeg‘⟨𝑘, 𝑒⟩)
95	94	fveq1i 6904	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣)
96	95	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ 𝑘 → ((𝑘VtxDeg𝑒)‘𝑣) = ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣))
97	96	sumeq2i 15716	. . . . . . . . . . . . . . 15 ⊢ Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣)
98	97	eqeq1i 2734	. . . . . . . . . . . . . 14 ⊢ (Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒)) ↔ Σ𝑣 ∈ 𝑘 ((VtxDeg‘⟨𝑘, 𝑒⟩)‘𝑣) = (2 · (♯‘𝑒)))
99	93, 98	imbitrrdi 251	. . . . . . . . . . . . 13 ⊢ (((⟨𝑘, 𝑒⟩ ∈ UPGraph ∧ 𝑛 ∈ 𝑘) ∧ (𝑘 ∈ Fin ∧ 𝑒 ∈ Fin)) → ((((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)}) ∈ Fin → Σ𝑣 ∈ (𝑘 ∖ {𝑛})((VtxDeg‘⟨(𝑘 ∖ {𝑛}), ((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})⟩)‘𝑣) = (2 · (♯‘((iEdg‘⟨𝑘, 𝑒⟩) ↾ {𝑖 ∈ dom (iEdg‘⟨𝑘, 𝑒⟩) ∣ 𝑛 ∉ ((iEdg‘⟨𝑘, 𝑒⟩)‘𝑖)})))) → Σ𝑣 ∈ 𝑘 ((𝑘VtxDeg𝑒)‘𝑣) = (2 · (♯‘𝑒))))
100	99	exp32 419	. . . . . . . . . . . 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 1128	. . . . . . . . . 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 239	. . . . . . . 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 406	. . . . . . 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 405	. . . . . 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 14534	. . . . 5 ⊢ ((⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph ∧ (Vtx‘𝐺) ∈ Fin) → ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
108	107	ex 411	. . . 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 2820	. . . 4 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
112	111	a1i 11	. . 3 ⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin))
113		sumvtxdg2size.i	. . . . . 6 ⊢ 𝐼 = (iEdg‘𝐺)
114	113	eleq1i 2820	. . . . 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 29449	. . . . . . . . 9 ⊢ (𝐺 ∈ UPGraph → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
119	117, 118	eqtrid 2781	. . . . . . . 8 ⊢ (𝐺 ∈ UPGraph → 𝐷 = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺)))
120	119	fveq1d 6905	. . . . . . 7 ⊢ (𝐺 ∈ UPGraph → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
121	120	adantr 479	. . . . . 6 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑣 ∈ 𝑉) → (𝐷‘𝑣) = (((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
122	116, 121	sumeq12dv 15723	. . . . 5 ⊢ (𝐺 ∈ UPGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣))
123	113	fveq2i 6906	. . . . . . 7 ⊢ (♯‘𝐼) = (♯‘(iEdg‘𝐺))
124	123	oveq2i 7438	. . . . . 6 ⊢ (2 · (♯‘𝐼)) = (2 · (♯‘(iEdg‘𝐺)))
125	124	a1i 11	. . . . 5 ⊢ (𝐺 ∈ UPGraph → (2 · (♯‘𝐼)) = (2 · (♯‘(iEdg‘𝐺))))
126	122, 125	eqeq12d 2745	. . . 4 ⊢ (𝐺 ∈ UPGraph → (Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)) ↔ Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺)))))
127	115, 126	imbi12d 343	. . 3 ⊢ (𝐺 ∈ UPGraph → ((𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) ↔ ((iEdg‘𝐺) ∈ Fin → Σ𝑣 ∈ (Vtx‘𝐺)(((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))‘𝑣) = (2 · (♯‘(iEdg‘𝐺))))))
128	109, 112, 127	3imtr4d 293	. 2 ⊢ (𝐺 ∈ UPGraph → (𝑉 ∈ Fin → (𝐼 ∈ Fin → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))))
129	128	3imp 1108	1 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2100   ∉ wnel 3039  {crab 3428  Vcvv 3472   ∖ cdif 3955  ∅c0 4333  {csn 4634  ⟨cop 4640  dom cdm 5684   ↾ cres 5686  ‘cfv 6556  (class class class)co 7427  Fincfn 8978  0cc0 11159  1c1 11160   + caddc 11162   · cmul 11164  2c2 12323  ℕ₀cn0 12528  ♯chash 14353  Σcsu 15703  Vtxcvtx 28974  iEdgciedg 28975  UHGraphcuhgr 29034  UPGraphcupgr 29058  VtxDegcvtxdg 29444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-inf2 9685  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236  ax-pre-sup 11237

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-pss 3978  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-int 4958  df-iun 5006  df-disj 5122  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-se 5640  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-isom 6565  df-riota 7383  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7882  df-1st 8008  df-2nd 8009  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-1o 8500  df-2o 8501  df-oadd 8504  df-er 8738  df-en 8979  df-dom 8980  df-sdom 8981  df-fin 8982  df-sup 9486  df-oi 9554  df-dju 9945  df-card 9983  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11497  df-neg 11498  df-div 11923  df-nn 12269  df-2 12331  df-3 12332  df-n0 12529  df-xnn0 12601  df-z 12615  df-uz 12879  df-rp 13033  df-xadd 13151  df-fz 13543  df-fzo 13686  df-seq 14027  df-exp 14087  df-hash 14354  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254  df-clim 15503  df-sum 15704  df-vtx 28976  df-iedg 28977  df-edg 29026  df-uhgr 29036  df-upgr 29060  df-vtxdg 29445

This theorem is referenced by:  fusgr1th  29530  finsumvtxdgeven  29531