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	$⊢ φ \to A \in Fin$
	regsumfsum.2	$⊢ (φ \land k \in A) \to B \in ℝ$
Assertion	regsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld} ↾_{𝑠} ℝ}} B = \sum_{k \in A} B$

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

Metamath Proof Explorer