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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
mbfpos.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
Assertion mbfpos ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 mbfpos.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
3 c0ex ⊢ 0 ∈ V
4 3 fvconst2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
5 4 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
7 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8 7 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9 6 1 8 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
10 5 9 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 0 ≤ 𝐵 ) )
11 10 9 5 ifbieq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
12 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
13 0re ⊢ 0 ∈ ℝ
14 13 fconst6 ⊢ ( 𝐴 × { 0 } ) : 𝐴 ⟶ ℝ
15 14 a1i ⊢ ( 𝜑 → ( 𝐴 × { 0 } ) : 𝐴 ⟶ ℝ )
16 2 1 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
17 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
18 mbfconst ⊢ ( ( 𝐴 ∈ dom vol ∧ 0 ∈ ℂ ) → ( 𝐴 × { 0 } ) ∈ MblFn )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 × { 0 } ) ∈ MblFn )
20 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
21 nfcv ⊢ Ⅎ 𝑦 if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) )
22 nfcv ⊢ Ⅎ 𝑥 ( ( 𝐴 × { 0 } ) ‘ 𝑦 )
23 nfcv ⊢ Ⅎ 𝑥 ≤
24 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
25 22 23 24 nfbr ⊢ Ⅎ 𝑥 ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
26 25 24 22 nfif ⊢ Ⅎ 𝑥 if ( ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) )
27 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) )
28 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
29 27 28 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) )
30 29 28 27 ifbieq12d ⊢ ( 𝑥 = 𝑦 → if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) = if ( ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ) )
31 21 26 30 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ if ( ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑦 ) ) )
32 15 19 20 2 31 mbfmax ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) ) ) ∈ MblFn )
33 12 32 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )