MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  finsumvtxdg2ssteplem4 Structured version   Visualization version   GIF version

Theorem finsumvtxdg2ssteplem4 26500
Description: Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 12-Dec-2021.)
Hypotheses
Ref Expression
finsumvtxdg2sstep.v 𝑉 = (Vtx‘𝐺)
finsumvtxdg2sstep.e 𝐸 = (iEdg‘𝐺)
finsumvtxdg2sstep.k 𝐾 = (𝑉 ∖ {𝑁})
finsumvtxdg2sstep.i 𝐼 = {𝑖 ∈ dom 𝐸𝑁 ∉ (𝐸𝑖)}
finsumvtxdg2sstep.p 𝑃 = (𝐸𝐼)
finsumvtxdg2sstep.s 𝑆 = ⟨𝐾, 𝑃
finsumvtxdg2ssteplem.j 𝐽 = {𝑖 ∈ dom 𝐸𝑁 ∈ (𝐸𝑖)}
Assertion
Ref Expression
finsumvtxdg2ssteplem4 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽))))
Distinct variable groups:   𝑖,𝐸   𝑖,𝐺   𝑖,𝑁   𝑣,𝐸   𝑣,𝐺   𝑣,𝑁   𝑖,𝑉,𝑣   𝑖,𝐽   𝑣,𝐾
Allowed substitution hints:   𝑃(𝑣,𝑖)   𝑆(𝑣,𝑖)   𝐼(𝑣,𝑖)   𝐽(𝑣)   𝐾(𝑖)

Proof of Theorem finsumvtxdg2ssteplem4
StepHypRef Expression
1 finsumvtxdg2sstep.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
2 finsumvtxdg2sstep.e . . . . . . . 8 𝐸 = (iEdg‘𝐺)
3 finsumvtxdg2sstep.k . . . . . . . 8 𝐾 = (𝑉 ∖ {𝑁})
4 finsumvtxdg2sstep.i . . . . . . . 8 𝐼 = {𝑖 ∈ dom 𝐸𝑁 ∉ (𝐸𝑖)}
5 finsumvtxdg2sstep.p . . . . . . . 8 𝑃 = (𝐸𝐼)
6 finsumvtxdg2sstep.s . . . . . . . 8 𝑆 = ⟨𝐾, 𝑃
7 finsumvtxdg2ssteplem.j . . . . . . . 8 𝐽 = {𝑖 ∈ dom 𝐸𝑁 ∈ (𝐸𝑖)}
81, 2, 3, 4, 5, 6, 7vtxdginducedm1fi 26496 . . . . . . 7 (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
98ad2antll 765 . . . . . 6 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
109sumeq2d 14476 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = Σ𝑣 ∈ (𝑉 ∖ {𝑁})(((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
11 diffi 8233 . . . . . . . 8 (𝑉 ∈ Fin → (𝑉 ∖ {𝑁}) ∈ Fin)
1211adantr 480 . . . . . . 7 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → (𝑉 ∖ {𝑁}) ∈ Fin)
1312adantl 481 . . . . . 6 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (𝑉 ∖ {𝑁}) ∈ Fin)
145dmeqi 5357 . . . . . . . . 9 dom 𝑃 = dom (𝐸𝐼)
15 finresfin 8227 . . . . . . . . . 10 (𝐸 ∈ Fin → (𝐸𝐼) ∈ Fin)
16 dmfi 8285 . . . . . . . . . 10 ((𝐸𝐼) ∈ Fin → dom (𝐸𝐼) ∈ Fin)
1715, 16syl 17 . . . . . . . . 9 (𝐸 ∈ Fin → dom (𝐸𝐼) ∈ Fin)
1814, 17syl5eqel 2734 . . . . . . . 8 (𝐸 ∈ Fin → dom 𝑃 ∈ Fin)
1918ad2antll 765 . . . . . . 7 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → dom 𝑃 ∈ Fin)
203eqcomi 2660 . . . . . . . . 9 (𝑉 ∖ {𝑁}) = 𝐾
2120eleq2i 2722 . . . . . . . 8 (𝑣 ∈ (𝑉 ∖ {𝑁}) ↔ 𝑣𝐾)
2221biimpi 206 . . . . . . 7 (𝑣 ∈ (𝑉 ∖ {𝑁}) → 𝑣𝐾)
236fveq2i 6232 . . . . . . . . . 10 (Vtx‘𝑆) = (Vtx‘⟨𝐾, 𝑃⟩)
241fvexi 6240 . . . . . . . . . . . . 13 𝑉 ∈ V
2524difexi 4842 . . . . . . . . . . . 12 (𝑉 ∖ {𝑁}) ∈ V
263, 25eqeltri 2726 . . . . . . . . . . 11 𝐾 ∈ V
272fvexi 6240 . . . . . . . . . . . . 13 𝐸 ∈ V
2827resex 5478 . . . . . . . . . . . 12 (𝐸𝐼) ∈ V
295, 28eqeltri 2726 . . . . . . . . . . 11 𝑃 ∈ V
3026, 29opvtxfvi 25934 . . . . . . . . . 10 (Vtx‘⟨𝐾, 𝑃⟩) = 𝐾
3123, 30eqtr2i 2674 . . . . . . . . 9 𝐾 = (Vtx‘𝑆)
321, 2, 3, 4, 5, 6vtxdginducedm1lem1 26491 . . . . . . . . . 10 (iEdg‘𝑆) = 𝑃
3332eqcomi 2660 . . . . . . . . 9 𝑃 = (iEdg‘𝑆)
34 eqid 2651 . . . . . . . . 9 dom 𝑃 = dom 𝑃
3531, 33, 34vtxdgfisnn0 26427 . . . . . . . 8 ((dom 𝑃 ∈ Fin ∧ 𝑣𝐾) → ((VtxDeg‘𝑆)‘𝑣) ∈ ℕ0)
3635nn0cnd 11391 . . . . . . 7 ((dom 𝑃 ∈ Fin ∧ 𝑣𝐾) → ((VtxDeg‘𝑆)‘𝑣) ∈ ℂ)
3719, 22, 36syl2an 493 . . . . . 6 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → ((VtxDeg‘𝑆)‘𝑣) ∈ ℂ)
38 dmfi 8285 . . . . . . . . . . . 12 (𝐸 ∈ Fin → dom 𝐸 ∈ Fin)
39 rabfi 8226 . . . . . . . . . . . 12 (dom 𝐸 ∈ Fin → {𝑖 ∈ dom 𝐸𝑁 ∈ (𝐸𝑖)} ∈ Fin)
4038, 39syl 17 . . . . . . . . . . 11 (𝐸 ∈ Fin → {𝑖 ∈ dom 𝐸𝑁 ∈ (𝐸𝑖)} ∈ Fin)
417, 40syl5eqel 2734 . . . . . . . . . 10 (𝐸 ∈ Fin → 𝐽 ∈ Fin)
42 rabfi 8226 . . . . . . . . . 10 (𝐽 ∈ Fin → {𝑖𝐽𝑣 ∈ (𝐸𝑖)} ∈ Fin)
43 hashcl 13185 . . . . . . . . . 10 ({𝑖𝐽𝑣 ∈ (𝐸𝑖)} ∈ Fin → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℕ0)
4441, 42, 433syl 18 . . . . . . . . 9 (𝐸 ∈ Fin → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℕ0)
4544nn0cnd 11391 . . . . . . . 8 (𝐸 ∈ Fin → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
4645ad2antll 765 . . . . . . 7 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
4746adantr 480 . . . . . 6 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
4813, 37, 47fsumadd 14514 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})(((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) = (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
4910, 48eqtrd 2685 . . . 4 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
503sumeq1i 14472 . . . . . 6 Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣)
5150eqeq1i 2656 . . . . 5 𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃)) ↔ Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃)))
52 oveq1 6697 . . . . 5 𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) = ((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
5351, 52sylbi 207 . . . 4 𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝑆)‘𝑣) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) = ((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
5449, 53sylan9eq 2705 . . 3 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = ((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})))
5554oveq1d 6705 . 2 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))))
5645adantl 481 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
5756adantr 480 . . . . . . . . 9 (((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ (𝑉 ∖ {𝑁})) → (#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
5812, 57fsumcl 14508 . . . . . . . 8 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
59 hashcl 13185 . . . . . . . . . . 11 (𝐽 ∈ Fin → (#‘𝐽) ∈ ℕ0)
6041, 59syl 17 . . . . . . . . . 10 (𝐸 ∈ Fin → (#‘𝐽) ∈ ℕ0)
6160nn0cnd 11391 . . . . . . . . 9 (𝐸 ∈ Fin → (#‘𝐽) ∈ ℂ)
6261adantl 481 . . . . . . . 8 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → (#‘𝐽) ∈ ℂ)
63 rabfi 8226 . . . . . . . . . . 11 (dom 𝐸 ∈ Fin → {𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}} ∈ Fin)
64 hashcl 13185 . . . . . . . . . . 11 ({𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}} ∈ Fin → (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}) ∈ ℕ0)
6538, 63, 643syl 18 . . . . . . . . . 10 (𝐸 ∈ Fin → (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}) ∈ ℕ0)
6665nn0cnd 11391 . . . . . . . . 9 (𝐸 ∈ Fin → (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}) ∈ ℂ)
6766adantl 481 . . . . . . . 8 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}) ∈ ℂ)
6858, 62, 67add12d 10300 . . . . . . 7 ((𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = ((#‘𝐽) + (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))))
6968adantl 481 . . . . . 6 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = ((#‘𝐽) + (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))))
701, 2, 3, 4, 5, 6, 7finsumvtxdg2ssteplem3 26499 . . . . . . 7 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}})) = (#‘𝐽))
7170oveq2d 6706 . . . . . 6 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((#‘𝐽) + (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = ((#‘𝐽) + (#‘𝐽)))
72612timesd 11313 . . . . . . . 8 (𝐸 ∈ Fin → (2 · (#‘𝐽)) = ((#‘𝐽) + (#‘𝐽)))
7372eqcomd 2657 . . . . . . 7 (𝐸 ∈ Fin → ((#‘𝐽) + (#‘𝐽)) = (2 · (#‘𝐽)))
7473ad2antll 765 . . . . . 6 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((#‘𝐽) + (#‘𝐽)) = (2 · (#‘𝐽)))
7569, 71, 743eqtrd 2689 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (2 · (#‘𝐽)))
7675oveq2d 6706 . . . 4 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((2 · (#‘𝑃)) + (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}})))) = ((2 · (#‘𝑃)) + (2 · (#‘𝐽))))
77 2cnd 11131 . . . . . . 7 (𝐸 ∈ Fin → 2 ∈ ℂ)
785, 15syl5eqel 2734 . . . . . . . . 9 (𝐸 ∈ Fin → 𝑃 ∈ Fin)
79 hashcl 13185 . . . . . . . . 9 (𝑃 ∈ Fin → (#‘𝑃) ∈ ℕ0)
8078, 79syl 17 . . . . . . . 8 (𝐸 ∈ Fin → (#‘𝑃) ∈ ℕ0)
8180nn0cnd 11391 . . . . . . 7 (𝐸 ∈ Fin → (#‘𝑃) ∈ ℂ)
8277, 81mulcld 10098 . . . . . 6 (𝐸 ∈ Fin → (2 · (#‘𝑃)) ∈ ℂ)
8382ad2antll 765 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (2 · (#‘𝑃)) ∈ ℂ)
8458adantl 481 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) ∈ ℂ)
8561, 66addcld 10097 . . . . . 6 (𝐸 ∈ Fin → ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}})) ∈ ℂ)
8685ad2antll 765 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}})) ∈ ℂ)
8783, 84, 86addassd 10100 . . . 4 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = ((2 · (#‘𝑃)) + (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)}) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}})))))
88 2cnd 11131 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → 2 ∈ ℂ)
8981ad2antll 765 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘𝑃) ∈ ℂ)
9061ad2antll 765 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘𝐽) ∈ ℂ)
9188, 89, 90adddid 10102 . . . 4 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (2 · ((#‘𝑃) + (#‘𝐽))) = ((2 · (#‘𝑃)) + (2 · (#‘𝐽))))
9276, 87, 913eqtr4d 2695 . . 3 (((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽))))
9392adantr 480 . 2 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (((2 · (#‘𝑃)) + Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖𝐽𝑣 ∈ (𝐸𝑖)})) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽))))
9455, 93eqtrd 2685 1 ((((𝐺 ∈ UPGraph ∧ 𝑁𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wnel 2926  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  {csn 4210  cop 4216  dom cdm 5143  cres 5145  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972   + caddc 9977   · cmul 9979  2c2 11108  0cn0 11330  #chash 13157  Σcsu 14460  Vtxcvtx 25919  iEdgciedg 25920  UPGraphcupgr 26020  VtxDegcvtxdg 26417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-xadd 11985  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-vtx 25921  df-iedg 25922  df-edg 25985  df-uhgr 25998  df-upgr 26022  df-vtxdg 26418
This theorem is referenced by:  finsumvtxdg2sstep  26501
  Copyright terms: Public domain W3C validator