mbfpos

Description: The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014)

	Ref	Expression
Hypotheses	mbfpos.1	$⊢ (φ \land x \in A) \to B \in ℝ$
	mbfpos.2	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
Assertion	mbfpos	$⊢ φ \to (x \in A ⟼ if (0 \leq B, B, 0)) \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfpos.1	$⊢ (φ \land x \in A) \to B \in ℝ$
2		mbfpos.2	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
3		c0ex	$⊢ 0 \in V$
4	3	fvconst2	$⊢ x \in A \to (A \times \{0\}) (x) = 0$
5	4	adantl	$⊢ (φ \land x \in A) \to (A \times \{0\}) (x) = 0$
6		simpr	$⊢ (φ \land x \in A) \to x \in A$
7		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
8	7	fvmpt2	$⊢ (x \in A \land B \in ℝ) \to (x \in A ⟼ B) (x) = B$
9	6 1 8	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
10	5 9	breq12d	$⊢ (φ \land x \in A) \to ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x) \leftrightarrow 0 \leq B)$
11	10 9 5	ifbieq12d	$⊢ (φ \land x \in A) \to if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x)) = if (0 \leq B, B, 0)$
12	11	mpteq2dva	$⊢ φ \to (x \in A ⟼ if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x))) = (x \in A ⟼ if (0 \leq B, B, 0))$
13		0re	$⊢ 0 \in ℝ$
14	13	fconst6	$⊢ (A \times \{0\}) : A ⟶ ℝ$
15	14	a1i	$⊢ φ \to (A \times \{0\}) : A ⟶ ℝ$
16	2 1	mbfdm2	$⊢ φ \to A \in dom vol$
17		0cnd	$⊢ φ \to 0 \in ℂ$
18		mbfconst	$⊢ (A \in dom vol \land 0 \in ℂ) \to A \times \{0\} \in MblFn$
19	16 17 18	syl2anc	$⊢ φ \to A \times \{0\} \in MblFn$
20	1	fmpttd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ$
21		nfcv	$⊢ \underline{Ⅎ} y if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x))$
22		nfcv	$⊢ \underline{Ⅎ} x (A \times \{0\}) (y)$
23		nfcv	$⊢ \underline{Ⅎ} x \leq$
24		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
25	22 23 24	nfbr	$⊢ Ⅎ x (A \times \{0\}) (y) \leq (x \in A ⟼ B) (y)$
26	25 24 22	nfif	$⊢ \underline{Ⅎ} x if ((A \times \{0\}) (y) \leq (x \in A ⟼ B) (y), (x \in A ⟼ B) (y), (A \times \{0\}) (y))$
27		fveq2	$⊢ x = y \to (A \times \{0\}) (x) = (A \times \{0\}) (y)$
28		fveq2	$⊢ x = y \to (x \in A ⟼ B) (x) = (x \in A ⟼ B) (y)$
29	27 28	breq12d	$⊢ x = y \to ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x) \leftrightarrow (A \times \{0\}) (y) \leq (x \in A ⟼ B) (y))$
30	29 28 27	ifbieq12d	$⊢ x = y \to if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x)) = if ((A \times \{0\}) (y) \leq (x \in A ⟼ B) (y), (x \in A ⟼ B) (y), (A \times \{0\}) (y))$
31	21 26 30	cbvmpt	$⊢ (x \in A ⟼ if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x))) = (y \in A ⟼ if ((A \times \{0\}) (y) \leq (x \in A ⟼ B) (y), (x \in A ⟼ B) (y), (A \times \{0\}) (y)))$
32	15 19 20 2 31	mbfmax	$⊢ φ \to (x \in A ⟼ if ((A \times \{0\}) (x) \leq (x \in A ⟼ B) (x), (x \in A ⟼ B) (x), (A \times \{0\}) (x))) \in MblFn$
33	12 32	eqeltrrd	$⊢ φ \to (x \in A ⟼ if (0 \leq B, B, 0)) \in MblFn$

Metamath Proof Explorer

Theorem mbfpos

Proof