bddibl

Description: A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

		Ref	Expression
	Assertion	bddibl	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
2	1	3ad2ant1	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to dom F \in dom vol$
3		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
4	3	3ad2ant1	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F : dom F ⟶ ℂ$
5	4	ffnd	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F Fn dom F$
6		1cnd	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to 1 \in ℂ$
7		fnconstg	$⊢ 1 \in ℂ \to (dom F \times \{1\}) Fn dom F$
8	6 7	syl	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to (dom F \times \{1\}) Fn dom F$
9		eqidd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \land z \in dom F) \to F (z) = F (z)$
10		1ex	$⊢ 1 \in V$
11	10	fvconst2	$⊢ z \in dom F \to (dom F \times \{1\}) (z) = 1$
12	11	adantl	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \land z \in dom F) \to (dom F \times \{1\}) (z) = 1$
13	4	ffvelcdmda	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \land z \in dom F) \to F (z) \in ℂ$
14	13	mulridd	$⊢ ((F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \land z \in dom F) \to F (z) \cdot 1 = F (z)$
15	2 5 8 5 9 12 14	offveq	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \times_{f} (dom F \times \{1\}) = F$
16		simp2	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to vol (dom F) \in ℝ$
17		iblconst	$⊢ (dom F \in dom vol \land vol (dom F) \in ℝ \land 1 \in ℂ) \to dom F \times \{1\} \in 𝐿^{1}$
18	2 16 6 17	syl3anc	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to dom F \times \{1\} \in 𝐿^{1}$
19		bddmulibl	$⊢ (F \in MblFn \land dom F \times \{1\} \in 𝐿^{1} \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \times_{f} (dom F \times \{1\}) \in 𝐿^{1}$
20	18 19	syld3an2	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \times_{f} (dom F \times \{1\}) \in 𝐿^{1}$
21	15 20	eqeltrrd	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem bddibl

Proof