itg1cl

Description: Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	itg1cl	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$

Step	Hyp	Ref	Expression
1		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
2		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
3		difss	$⊢ ran F ∖ \{0\} \subseteq ran F$
4		ssfi	$⊢ (ran F \in Fin \land ran F ∖ \{0\} \subseteq ran F) \to ran F ∖ \{0\} \in Fin$
5	2 3 4	sylancl	$⊢ F \in dom \int^{1} \to ran F ∖ \{0\} \in Fin$
6		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
7	6	frnd	$⊢ F \in dom \int^{1} \to ran F \subseteq ℝ$
8	7	ssdifssd	$⊢ F \in dom \int^{1} \to ran F ∖ \{0\} \subseteq ℝ$
9	8	sselda	$⊢ (F \in dom \int^{1} \land x \in (ran F ∖ \{0\})) \to x \in ℝ$
10		i1fima2sn	$⊢ (F \in dom \int^{1} \land x \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
11	9 10	remulcld	$⊢ (F \in dom \int^{1} \land x \in (ran F ∖ \{0\})) \to x vol (F^{-1} [\{x\}]) \in ℝ$
12	5 11	fsumrecl	$⊢ F \in dom \int^{1} \to \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}]) \in ℝ$
13	1 12	eqeltrd	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$

Metamath Proof Explorer