regsumsupp

Description: The group sum over the real numbers, expressed as a finite sum. (Contributed by Thierry Arnoux, 22-Jun-2019) (Proof shortened by AV, 19-Jul-2019)

		Ref	Expression
	Assertion	regsumsupp	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℝ_{fld}} F = \sum_{x \in F supp 0} F (x)$

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
2		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
3		cnring	$⊢ ℂ_{fld} \in Ring$
4		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
5	3 4	mp1i	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to ℂ_{fld} \in CMnd$
6		simp3	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to I \in V$
7		simp1	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to F : I ⟶ ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9		fss	$⊢ (F : I ⟶ ℝ \land ℝ \subseteq ℂ) \to F : I ⟶ ℂ$
10	7 8 9	sylancl	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to F : I ⟶ ℂ$
11		ssidd	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to F supp 0 \subseteq F supp 0$
12		simp2	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to {finSupp}_{0} (F)$
13	1 2 5 6 10 11 12	gsumres	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℂ_{fld}} ({F ↾}_{{supp}_{0} (F)}) = \sum_{ℂ_{fld}} F$
14		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
15		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
16	8	a1i	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to ℝ \subseteq ℂ$
17		0red	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to 0 \in ℝ$
18		simpr	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in ℂ) \to x \in ℂ$
19	18	addid2d	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in ℂ) \to 0 + x = x$
20	18	addid1d	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in ℂ) \to x + 0 = x$
21	19 20	jca	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in ℂ) \to (0 + x = x \land x + 0 = x)$
22	1 14 15 5 6 16 7 17 21	gsumress	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℂ_{fld}} F = \sum_{ℝ_{fld}} F$
23	13 22	eqtr2d	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℝ_{fld}} F = \sum_{ℂ_{fld}} ({F ↾}_{{supp}_{0} (F)})$
24		suppssdm	$⊢ F supp 0 \subseteq dom F$
25	24 7	fssdm	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to F supp 0 \subseteq I$
26	7 25	feqresmpt	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to {F ↾}_{{supp}_{0} (F)} = (x \in {supp}_{0} (F) ⟼ F (x))$
27	26	oveq2d	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℂ_{fld}} ({F ↾}_{{supp}_{0} (F)}) = \underset{x \in F supp 0}{\sum_{ℂ_{fld}}} F (x)$
28	12	fsuppimpd	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to F supp 0 \in Fin$
29		simpl1	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in {supp}_{0} (F)) \to F : I ⟶ ℝ$
30	25	sselda	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in {supp}_{0} (F)) \to x \in I$
31	29 30	ffvelrnd	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in {supp}_{0} (F)) \to F (x) \in ℝ$
32	8 31	sseldi	$⊢ ((F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \land x \in {supp}_{0} (F)) \to F (x) \in ℂ$
33	28 32	gsumfsum	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \underset{x \in F supp 0}{\sum_{ℂ_{fld}}} F (x) = \sum_{x \in F supp 0} F (x)$
34	23 27 33	3eqtrd	$⊢ (F : I ⟶ ℝ \land {finSupp}_{0} (F) \land I \in V) \to \sum_{ℝ_{fld}} F = \sum_{x \in F supp 0} F (x)$

Metamath Proof Explorer

Theorem regsumsupp

Proof