itg1val

Description: The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014)

		Ref	Expression
	Assertion	itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$

Step	Hyp	Ref	Expression
1		rneq	$⊢ f = F \to ran f = ran F$
2	1	difeq1d	$⊢ f = F \to ran f ∖ \{0\} = ran F ∖ \{0\}$
3		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
4	3	imaeq1d	$⊢ f = F \to f^{-1} [\{x\}] = F^{-1} [\{x\}]$
5	4	fveq2d	$⊢ f = F \to vol (f^{-1} [\{x\}]) = vol (F^{-1} [\{x\}])$
6	5	oveq2d	$⊢ f = F \to x vol (f^{-1} [\{x\}]) = x vol (F^{-1} [\{x\}])$
7	6	adantr	$⊢ (f = F \land x \in (ran f ∖ \{0\})) \to x vol (f^{-1} [\{x\}]) = x vol (F^{-1} [\{x\}])$
8	2 7	sumeq12dv	$⊢ f = F \to \sum_{x \in ran f ∖ \{0\}} x vol (f^{-1} [\{x\}]) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
9		df-itg1	$⊢ \int^{1} = (f \in \{g \in MblFn \| (g : ℝ ⟶ ℝ \land ran g \in Fin \land vol (g^{-1} [ℝ ∖ \{0\}]) \in ℝ)\} ⟼ \sum_{x \in ran f ∖ \{0\}} x vol (f^{-1} [\{x\}]))$
10		sumex	$⊢ \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}]) \in V$
11	8 9 10	fvmpt	$⊢ F \in \{g \in MblFn \| (g : ℝ ⟶ ℝ \land ran g \in Fin \land vol (g^{-1} [ℝ ∖ \{0\}]) \in ℝ)\} \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
12		sumex	$⊢ \sum_{x \in ran f ∖ \{0\}} x vol (f^{-1} [\{x\}]) \in V$
13	12 9	dmmpti	$⊢ dom \int^{1} = \{g \in MblFn \| (g : ℝ ⟶ ℝ \land ran g \in Fin \land vol (g^{-1} [ℝ ∖ \{0\}]) \in ℝ)\}$
14	11 13	eleq2s	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$

Metamath Proof Explorer