# Metamath Proof Explorer

## Theorem esumeq2

Description: Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016)

Ref Expression
Assertion esumeq2 ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\underset{{k}\in {A}}{{\sum }^{*}}{C}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{A}={A}$
2 mpteq12 ${⊢}\left({A}={A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\right)\to \left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{C}\right)$
3 1 2 mpan ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{C}\right)$
4 3 oveq2d ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)=\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{C}\right)$
5 4 unieqd ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)\right)=\bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{C}\right)\right)$
6 df-esum ${⊢}\underset{{k}\in {A}}{{\sum }^{*}}{B}=\bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{B}\right)\right)$
7 df-esum ${⊢}\underset{{k}\in {A}}{{\sum }^{*}}{C}=\bigcup \left(\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left({k}\in {A}⟼{C}\right)\right)$
8 5 6 7 3eqtr4g ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\underset{{k}\in {A}}{{\sum }^{*}}{C}$