Theorem regsumfsum

Description: Relate a group sum on ` ( CCfld |``s RR ) ` to a finite sum on the reals. Cf. gsumfsum . (Contributed by Thierry Arnoux, 7-Sep-2018)

	Ref	Expression
Hypotheses	regsumfsum.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	regsumfsum.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
Assertion	regsumfsum	$$⊢\phi \to \underset{k\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ}}B=\sum _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		regsumfsum.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		regsumfsum.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
5		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
6		cnfldex	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{V}$$
8		ax-resscn	$$⊢ℝ\subseteq ℂ$$
9	8	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
10	2	fmpttd	$$⊢\phi \to \left(k\in A⟼B\right):A⟶ℝ$$
11		0red	$$⊢\phi \to 0\in ℝ$$
12		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
13	12	addid2d	$$⊢\left(\phi \wedge x\in ℂ\right)\to 0+x=x$$
14	12	addid1d	$$⊢\left(\phi \wedge x\in ℂ\right)\to x+0=x$$
15	13 14	jca	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(0+x=x\wedge x+0=x\right)$$
16	3 4 5 7 1 9 10 11 15	gsumress	$$⊢\phi \to \underset{k\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}B=\underset{k\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ}}B$$
17	2	recnd	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
18	1 17	gsumfsum	$$⊢\phi \to \underset{k\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}B=\sum _{k\in A}B$$
19	16 18	eqtr3d	$$⊢\phi \to \underset{k\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ}}B=\sum _{k\in A}B$$