itg1val2

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

		Ref	Expression
	Assertion	itg1val2	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to \int^{1} (F) = \sum_{x \in A} x vol (F^{-1} [\{x\}])$

Proof

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	1	adantr	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to \int^{1} (F) = \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}])$
3		simpr2	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to ran F ∖ \{0\} \subseteq A$
4	3	sselda	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (ran F ∖ \{0\})) \to x \in A$
5		simpr3	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to A \subseteq ℝ ∖ \{0\}$
6	5	sselda	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in A) \to x \in (ℝ ∖ \{0\})$
7		eldifi	$⊢ x \in (ℝ ∖ \{0\}) \to x \in ℝ$
8	6 7	syl	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in A) \to x \in ℝ$
9		i1fima2sn	$⊢ (F \in dom \int^{1} \land x \in (ℝ ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
10	9	adantlr	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (ℝ ∖ \{0\})) \to vol (F^{-1} [\{x\}]) \in ℝ$
11	6 10	syldan	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in A) \to vol (F^{-1} [\{x\}]) \in ℝ$
12	8 11	remulcld	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in A) \to x vol (F^{-1} [\{x\}]) \in ℝ$
13	12	recnd	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in A) \to x vol (F^{-1} [\{x\}]) \in ℂ$
14	4 13	syldan	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (ran F ∖ \{0\})) \to x vol (F^{-1} [\{x\}]) \in ℂ$
15		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
16	15	ad2antrr	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to F : ℝ ⟶ ℝ$
17		ffrn	$⊢ F : ℝ ⟶ ℝ \to F : ℝ ⟶ ran F$
18	16 17	syl	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to F : ℝ ⟶ ran F$
19		eldifn	$⊢ x \in (A ∖ (ran F ∖ \{0\})) \to \neg x \in (ran F ∖ \{0\})$
20	19	adantl	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to \neg x \in (ran F ∖ \{0\})$
21		eldif	$⊢ x \in (ran F ∖ \{0\}) \leftrightarrow (x \in ran F \land \neg x \in \{0\})$
22		simplr3	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to A \subseteq ℝ ∖ \{0\}$
23	22	ssdifssd	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to A ∖ (ran F ∖ \{0\}) \subseteq ℝ ∖ \{0\}$
24		simpr	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x \in (A ∖ (ran F ∖ \{0\}))$
25	23 24	sseldd	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x \in (ℝ ∖ \{0\})$
26		eldifn	$⊢ x \in (ℝ ∖ \{0\}) \to \neg x \in \{0\}$
27	25 26	syl	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to \neg x \in \{0\}$
28	27	biantrud	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to (x \in ran F \leftrightarrow (x \in ran F \land \neg x \in \{0\}))$
29	21 28	bitr4id	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to (x \in (ran F ∖ \{0\}) \leftrightarrow x \in ran F)$
30	20 29	mtbid	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to \neg x \in ran F$
31		disjsn	$⊢ ran F \cap \{x\} = \emptyset \leftrightarrow \neg x \in ran F$
32	30 31	sylibr	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to ran F \cap \{x\} = \emptyset$
33		fimacnvdisj	$⊢ (F : ℝ ⟶ ran F \land ran F \cap \{x\} = \emptyset) \to F^{-1} [\{x\}] = \emptyset$
34	18 32 33	syl2anc	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to F^{-1} [\{x\}] = \emptyset$
35	34	fveq2d	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to vol (F^{-1} [\{x\}]) = vol (\emptyset)$
36		0mbl	$⊢ \emptyset \in dom vol$
37		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
38	36 37	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
39		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
40	38 39	eqtri	$⊢ vol (\emptyset) = 0$
41	35 40	eqtrdi	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to vol (F^{-1} [\{x\}]) = 0$
42	41	oveq2d	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x vol (F^{-1} [\{x\}]) = x \cdot 0$
43		eldifi	$⊢ x \in (A ∖ (ran F ∖ \{0\})) \to x \in A$
44	43 8	sylan2	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x \in ℝ$
45	44	recnd	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x \in ℂ$
46	45	mul01d	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x \cdot 0 = 0$
47	42 46	eqtrd	$⊢ ((F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \land x \in (A ∖ (ran F ∖ \{0\}))) \to x vol (F^{-1} [\{x\}]) = 0$
48		simpr1	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to A \in Fin$
49	3 14 47 48	fsumss	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to \sum_{x \in ran F ∖ \{0\}} x vol (F^{-1} [\{x\}]) = \sum_{x \in A} x vol (F^{-1} [\{x\}])$
50	2 49	eqtrd	$⊢ (F \in dom \int^{1} \land (A \in Fin \land ran F ∖ \{0\} \subseteq A \land A \subseteq ℝ ∖ \{0\})) \to \int^{1} (F) = \sum_{x \in A} x vol (F^{-1} [\{x\}])$

Metamath Proof Explorer

Theorem itg1val2

Proof