Metamath Proof Explorer

Theorem esumc

Description: Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses esumc.0 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
esumc.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
esumc.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
esumc.3 ${⊢}{y}={C}\to {D}={B}$
esumc.4 ${⊢}{\phi }\to {A}\in {V}$
esumc.5 ${⊢}{\phi }\to \mathrm{Fun}{\left({k}\in {A}⟼{C}\right)}^{-1}$
esumc.6 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
esumc.7 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in {W}$
Assertion esumc ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\underset{{y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}}{{\sum }^{*}}{D}$

Proof

Step Hyp Ref Expression
1 esumc.0 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{D}$
2 esumc.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
3 esumc.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
4 esumc.3 ${⊢}{y}={C}\to {D}={B}$
5 esumc.4 ${⊢}{\phi }\to {A}\in {V}$
6 esumc.5 ${⊢}{\phi }\to \mathrm{Fun}{\left({k}\in {A}⟼{C}\right)}^{-1}$
7 esumc.6 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
8 esumc.7 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in {W}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
10 nfre1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}$
11 10 nfab ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
12 nfmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{C}\right)$
13 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
14 5 13 syl ${⊢}{\phi }\to {A}\in \mathrm{V}$
15 3 14 abrexexd ${⊢}{\phi }\to \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}\in \mathrm{V}$
16 8 ex ${⊢}{\phi }\to \left({k}\in {A}\to {C}\in {W}\right)$
17 2 16 ralrimi ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {W}$
18 3 fnmptf ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\in {W}\to \left({k}\in {A}⟼{C}\right)Fn{A}$
19 17 18 syl ${⊢}{\phi }\to \left({k}\in {A}⟼{C}\right)Fn{A}$
20 eqid ${⊢}\left({k}\in {A}⟼{C}\right)=\left({k}\in {A}⟼{C}\right)$
21 20 rnmpt ${⊢}\mathrm{ran}\left({k}\in {A}⟼{C}\right)=\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
22 21 a1i ${⊢}{\phi }\to \mathrm{ran}\left({k}\in {A}⟼{C}\right)=\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
23 dff1o2 ${⊢}\left({k}\in {A}⟼{C}\right):{A}\underset{1-1 onto}{⟶}\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}↔\left(\left({k}\in {A}⟼{C}\right)Fn{A}\wedge \mathrm{Fun}{\left({k}\in {A}⟼{C}\right)}^{-1}\wedge \mathrm{ran}\left({k}\in {A}⟼{C}\right)=\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}\right)$
24 19 6 22 23 syl3anbrc ${⊢}{\phi }\to \left({k}\in {A}⟼{C}\right):{A}\underset{1-1 onto}{⟶}\left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
25 simpr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {A}$
26 3 fvmpt2f ${⊢}\left({k}\in {A}\wedge {C}\in {W}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
27 25 8 26 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
28 vex ${⊢}{y}\in \mathrm{V}$
29 eqeq1 ${⊢}{z}={y}\to \left({z}={C}↔{y}={C}\right)$
30 29 rexbidv ${⊢}{z}={y}\to \left(\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}↔\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\right)$
31 28 30 elab ${⊢}{y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}↔\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}$
32 4 reximi ${⊢}\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{y}={C}\to \exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{D}={B}$
33 31 32 sylbi ${⊢}{y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}\to \exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{D}={B}$
34 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left[0,\mathrm{+\infty }\right]$
35 1 34 nfel ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{D}\in \left[0,\mathrm{+\infty }\right]$
36 eleq1 ${⊢}{D}={B}\to \left({D}\in \left[0,\mathrm{+\infty }\right]↔{B}\in \left[0,\mathrm{+\infty }\right]\right)$
37 7 36 syl5ibrcom ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({D}={B}\to {D}\in \left[0,\mathrm{+\infty }\right]\right)$
38 37 ex ${⊢}{\phi }\to \left({k}\in {A}\to \left({D}={B}\to {D}\in \left[0,\mathrm{+\infty }\right]\right)\right)$
39 2 35 38 rexlimd ${⊢}{\phi }\to \left(\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{D}={B}\to {D}\in \left[0,\mathrm{+\infty }\right]\right)$
40 39 imp ${⊢}\left({\phi }\wedge \exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{D}={B}\right)\to {D}\in \left[0,\mathrm{+\infty }\right]$
41 33 40 sylan2 ${⊢}\left({\phi }\wedge {y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}\right)\to {D}\in \left[0,\mathrm{+\infty }\right]$
42 2 1 9 11 3 12 4 15 24 27 41 esumf1o ${⊢}{\phi }\to \underset{{y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}}{{\sum }^{*}}{D}=\underset{{k}\in {A}}{{\sum }^{*}}{B}$
43 42 eqcomd ${⊢}{\phi }\to \underset{{k}\in {A}}{{\sum }^{*}}{B}=\underset{{y}\in \left\{{z}|\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}}{{\sum }^{*}}{D}$