Metamath Proof Explorer

Theorem sge0rnre

Description: When sum^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	sge0rnre.1	$⊢ φ \to F : X ⟶ [0, +∞)$
	Assertion	sge0rnre	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$

Proof

Step	Hyp	Ref	Expression
1		sge0rnre.1	$⊢ φ \to F : X ⟶ [0, +∞)$
2		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
3	2	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
4		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
5	1	ad2antrr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F : X ⟶ [0, +∞)$
6		elinel1	$⊢ x \in (𝒫 X \cap Fin) \to x \in 𝒫 X$
7		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
8	6 7	syl	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
9	8	adantr	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to x \subseteq X$
10		simpr	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to y \in x$
11	9 10	sseldd	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to y \in X$
12	11	adantll	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
13	5 12	ffvelcdmd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
14	4 13	sselid	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ$
15	3 14	fsumrecl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) \in ℝ$
16	15	ralrimiva	$⊢ φ \to \forall x \in (𝒫 X \cap Fin) \sum_{y \in x} F (y) \in ℝ$
17		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
18	17	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) \sum_{y \in x} F (y) \in ℝ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
19	16 18	syl	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$