Theorem mbfpos

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

	Ref	Expression
Hypotheses	mbfpos.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	mbfpos.2	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
Assertion	mbfpos	$$⊢\phi \to \left(x\in A⟼if\left(0\le B,B,0\right)\right)\in MblFn$$

Proof

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