ibl0

Description: The zero function is integrable on any measurable set. (Unlike iblconst , this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	ibl0	$⊢ A \in dom vol \to A \times \{0\} \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		mbfconst	$⊢ (A \in dom vol \land 0 \in ℂ) \to A \times \{0\} \in MblFn$
3	1 2	mpan2	$⊢ A \in dom vol \to A \times \{0\} \in MblFn$
4		ax-icn	$⊢ i \in ℂ$
5		ine0	$⊢ i \neq 0$
6		elfzelz	$⊢ k \in (0 \dots 3) \to k \in ℤ$
7	6	ad2antlr	$⊢ ((A \in dom vol \land k \in (0 \dots 3)) \land x \in A) \to k \in ℤ$
8		expclz	$⊢ (i \in ℂ \land i \neq 0 \land k \in ℤ) \to i^{k} \in ℂ$
9		expne0i	$⊢ (i \in ℂ \land i \neq 0 \land k \in ℤ) \to i^{k} \neq 0$
10	8 9	div0d	$⊢ (i \in ℂ \land i \neq 0 \land k \in ℤ) \to \frac{0}{i^{k}} = 0$
11	4 5 7 10	mp3an12i	$⊢ ((A \in dom vol \land k \in (0 \dots 3)) \land x \in A) \to \frac{0}{i^{k}} = 0$
12	11	fveq2d	$⊢ ((A \in dom vol \land k \in (0 \dots 3)) \land x \in A) \to ℜ (\frac{0}{i^{k}}) = ℜ (0)$
13		re0	$⊢ ℜ (0) = 0$
14	12 13	eqtrdi	$⊢ ((A \in dom vol \land k \in (0 \dots 3)) \land x \in A) \to ℜ (\frac{0}{i^{k}}) = 0$
15	14	itgvallem3	$⊢ (A \in dom vol \land k \in (0 \dots 3)) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0))) = 0$
16		0re	$⊢ 0 \in ℝ$
17	15 16	eqeltrdi	$⊢ (A \in dom vol \land k \in (0 \dots 3)) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0))) \in ℝ$
18	17	ralrimiva	$⊢ A \in dom vol \to \forall k \in (0 \dots 3) \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0))) \in ℝ$
19		eqidd	$⊢ A \in dom vol \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0)) = (x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0))$
20		eqidd	$⊢ (A \in dom vol \land x \in A) \to ℜ (\frac{0}{i^{k}}) = ℜ (\frac{0}{i^{k}})$
21		c0ex	$⊢ 0 \in V$
22	21	fconst	$⊢ (A \times \{0\}) : A ⟶ \{0\}$
23		fdm	$⊢ (A \times \{0\}) : A ⟶ \{0\} \to dom (A \times \{0\}) = A$
24	22 23	mp1i	$⊢ A \in dom vol \to dom (A \times \{0\}) = A$
25	21	fvconst2	$⊢ x \in A \to (A \times \{0\}) (x) = 0$
26	25	adantl	$⊢ (A \in dom vol \land x \in A) \to (A \times \{0\}) (x) = 0$
27	19 20 24 26	isibl	$⊢ A \in dom vol \to (A \times \{0\} \in 𝐿^{1} \leftrightarrow (A \times \{0\} \in MblFn \land \forall k \in (0 \dots 3) \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{0}{i^{k}})), ℜ (\frac{0}{i^{k}}), 0))) \in ℝ))$
28	3 18 27	mpbir2and	$⊢ A \in dom vol \to A \times \{0\} \in 𝐿^{1}$

Metamath Proof Explorer

Theorem ibl0

Proof