# Metamath Proof Explorer

## 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}×\left\{0\right\}\right)\left({x}\right)=0$
5 4 adantl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({A}×\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}×\left\{0\right\}\right)\left({x}\right)\le \left({x}\in {A}⟼{B}\right)\left({x}\right)↔0\le {B}\right)$
11 10 9 5 ifbieq12d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left(\left({A}×\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}×\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}×\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}×\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}×\left\{0\right\}\right):{A}⟶ℝ$
15 14 a1i ${⊢}{\phi }\to \left({A}×\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}×\left\{0\right\}\in MblFn$
19 16 17 18 syl2anc ${⊢}{\phi }\to {A}×\left\{0\right\}\in MblFn$
20 1 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℝ$
21 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}if\left(\left({A}×\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}×\left\{0\right\}\right)\left({x}\right)\right)$
22 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}×\left\{0\right\}\right)\left({y}\right)$
23 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\le$
24 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
25 22 23 24 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}×\left\{0\right\}\right)\left({y}\right)\le \left({x}\in {A}⟼{B}\right)\left({y}\right)$
26 25 24 22 nfif ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left(\left({A}×\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}×\left\{0\right\}\right)\left({y}\right)\right)$
27 fveq2 ${⊢}{x}={y}\to \left({A}×\left\{0\right\}\right)\left({x}\right)=\left({A}×\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}×\left\{0\right\}\right)\left({x}\right)\le \left({x}\in {A}⟼{B}\right)\left({x}\right)↔\left({A}×\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}×\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}×\left\{0\right\}\right)\left({x}\right)\right)=if\left(\left({A}×\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}×\left\{0\right\}\right)\left({y}\right)\right)$
31 21 26 30 cbvmpt ${⊢}\left({x}\in {A}⟼if\left(\left({A}×\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}×\left\{0\right\}\right)\left({x}\right)\right)\right)=\left({y}\in {A}⟼if\left(\left({A}×\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}×\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}×\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}×\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$