itg10a

Description: The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014)

	Ref	Expression
Hypotheses	itg10a.1	$⊢ φ \to F \in dom \int^{1}$
	itg10a.2	$⊢ φ \to A \subseteq ℝ$
	itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
	itg10a.4	$⊢ (φ \land x \in (ℝ ∖ A)) \to F (x) = 0$
Assertion	itg10a	$⊢ φ \to \int^{1} (F) = 0$

Proof

Step	Hyp	Ref	Expression
1		itg10a.1	$⊢ φ \to F \in dom \int^{1}$
2		itg10a.2	$⊢ φ \to A \subseteq ℝ$
3		itg10a.3	$⊢ φ \to {vol}^{*} (A) = 0$
4		itg10a.4	$⊢ (φ \land x \in (ℝ ∖ A)) \to F (x) = 0$
5		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
6	1 5	syl	$⊢ φ \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
7		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
8	1 7	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
9	8	ffnd	$⊢ φ \to F Fn ℝ$
10	9	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F Fn ℝ$
11		fniniseg	$⊢ F Fn ℝ \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
12	10 11	syl	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
13		eldifsni	$⊢ k \in (ran F ∖ \{0\}) \to k \neq 0$
14	13	ad2antlr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to k \neq 0$
15		simprl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to x \in ℝ$
16		eldif	$⊢ x \in (ℝ ∖ A) \leftrightarrow (x \in ℝ \land \neg x \in A)$
17		simplrr	$⊢ (((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \land x \in (ℝ ∖ A)) \to F (x) = k$
18	4	ad4ant14	$⊢ (((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \land x \in (ℝ ∖ A)) \to F (x) = 0$
19	17 18	eqtr3d	$⊢ (((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \land x \in (ℝ ∖ A)) \to k = 0$
20	19	ex	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (x \in (ℝ ∖ A) \to k = 0)$
21	16 20	syl5bir	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to ((x \in ℝ \land \neg x \in A) \to k = 0)$
22	15 21	mpand	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (\neg x \in A \to k = 0)$
23	22	necon1ad	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to (k \neq 0 \to x \in A)$
24	14 23	mpd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land (x \in ℝ \land F (x) = k)) \to x \in A$
25	24	ex	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ((x \in ℝ \land F (x) = k) \to x \in A)$
26	12 25	sylbid	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (x \in F^{-1} [\{k\}] \to x \in A)$
27	26	ssrdv	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \subseteq A$
28	2	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to A \subseteq ℝ$
29	27 28	sstrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \subseteq ℝ$
30	3	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to {vol}^{*} (A) = 0$
31		ovolssnul	$⊢ (F^{-1} [\{k\}] \subseteq A \land A \subseteq ℝ \land {vol}^{} (A) = 0) \to {vol}^{} (F^{-1} [\{k\}]) = 0$
32	27 28 30 31	syl3anc	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to {vol}^{*} (F^{-1} [\{k\}]) = 0$
33		nulmbl	$⊢ (F^{-1} [\{k\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{k\}]) = 0) \to F^{-1} [\{k\}] \in dom vol$
34	29 32 33	syl2anc	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \in dom vol$
35		mblvol	$⊢ F^{-1} [\{k\}] \in dom vol \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
36	34 35	syl	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
37	36 32	eqtrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) = 0$
38	37	oveq2d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k vol (F^{-1} [\{k\}]) = k \cdot 0$
39	8	frnd	$⊢ φ \to ran F \subseteq ℝ$
40	39	ssdifssd	$⊢ φ \to ran F ∖ \{0\} \subseteq ℝ$
41	40	sselda	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℝ$
42	41	recnd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℂ$
43	42	mul01d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \cdot 0 = 0$
44	38 43	eqtrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k vol (F^{-1} [\{k\}]) = 0$
45	44	sumeq2dv	$⊢ φ \to \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}]) = \sum_{k \in ran F ∖ \{0\}} 0$
46		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
47	1 46	syl	$⊢ φ \to ran F \in Fin$
48		difss	$⊢ ran F ∖ \{0\} \subseteq ran F$
49		ssfi	$⊢ (ran F \in Fin \land ran F ∖ \{0\} \subseteq ran F) \to ran F ∖ \{0\} \in Fin$
50	47 48 49	sylancl	$⊢ φ \to ran F ∖ \{0\} \in Fin$
51	50	olcd	$⊢ φ \to (ran F ∖ \{0\} \subseteq ℤ_{\geq 0} \lor ran F ∖ \{0\} \in Fin)$
52		sumz	$⊢ (ran F ∖ \{0\} \subseteq ℤ_{\geq 0} \lor ran F ∖ \{0\} \in Fin) \to \sum_{k \in ran F ∖ \{0\}} 0 = 0$
53	51 52	syl	$⊢ φ \to \sum_{k \in ran F ∖ \{0\}} 0 = 0$
54	45 53	eqtrd	$⊢ φ \to \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}]) = 0$
55	6 54	eqtrd	$⊢ φ \to \int^{1} (F) = 0$

Metamath Proof Explorer

Theorem itg10a

Proof