Metamath Proof Explorer

Theorem mbfposb

Description: A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypothesis mbfpos.1 ⊢φ∧x∈A→B∈ℝ
Assertion mbfposb ⊢φ→x∈A⟼B∈MblFn↔x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢φ∧x∈A→B∈ℝ
2 nfcv ⊢Ⅎ_x0
3 nfcv ⊢Ⅎ_x≤
4 nffvmpt1 ⊢Ⅎ_xx∈A⟼B⁡y
5 2 3 4 nfbr ⊢Ⅎx0≤x∈A⟼B⁡y
6 5 4 2 nfif ⊢Ⅎ_xif0≤x∈A⟼B⁡yx∈A⟼B⁡y0
7 nfcv ⊢Ⅎ_yif0≤x∈A⟼B⁡xx∈A⟼B⁡x0
8 fveq2 ⊢y=x→x∈A⟼B⁡y=x∈A⟼B⁡x
9 8 breq2d ⊢y=x→0≤x∈A⟼B⁡y↔0≤x∈A⟼B⁡x
10 9 8 ifbieq1d ⊢y=x→if0≤x∈A⟼B⁡yx∈A⟼B⁡y0=if0≤x∈A⟼B⁡xx∈A⟼B⁡x0
11 6 7 10 cbvmpt ⊢y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0=x∈A⟼if0≤x∈A⟼B⁡xx∈A⟼B⁡x0
12 simpr ⊢φ∧x∈A→x∈A
13 eqid ⊢x∈A⟼B=x∈A⟼B
14 13 fvmpt2 ⊢x∈A∧B∈ℝ→x∈A⟼B⁡x=B
15 12 1 14 syl2anc ⊢φ∧x∈A→x∈A⟼B⁡x=B
16 15 breq2d ⊢φ∧x∈A→0≤x∈A⟼B⁡x↔0≤B
17 16 15 ifbieq1d ⊢φ∧x∈A→if0≤x∈A⟼B⁡xx∈A⟼B⁡x0=if0≤BB0
18 17 mpteq2dva ⊢φ→x∈A⟼if0≤x∈A⟼B⁡xx∈A⟼B⁡x0=x∈A⟼if0≤BB0
19 11 18 eqtrid ⊢φ→y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0=x∈A⟼if0≤BB0
20 19 adantr ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0=x∈A⟼if0≤BB0
21 1 fmpttd ⊢φ→x∈A⟼B:A⟶ℝ
22 21 adantr ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼B:A⟶ℝ
23 22 ffvelrnda ⊢φ∧x∈A⟼B∈MblFn∧y∈A→x∈A⟼B⁡y∈ℝ
24 nfcv ⊢Ⅎ_yx∈A⟼B⁡x
25 4 24 8 cbvmpt ⊢y∈A⟼x∈A⟼B⁡y=x∈A⟼x∈A⟼B⁡x
26 15 mpteq2dva ⊢φ→x∈A⟼x∈A⟼B⁡x=x∈A⟼B
27 25 26 eqtrid ⊢φ→y∈A⟼x∈A⟼B⁡y=x∈A⟼B
28 27 eleq1d ⊢φ→y∈A⟼x∈A⟼B⁡y∈MblFn↔x∈A⟼B∈MblFn
29 28 biimpar ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼x∈A⟼B⁡y∈MblFn
30 23 29 mbfpos ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0∈MblFn
31 20 30 eqeltrrd ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼if0≤BB0∈MblFn
32 4 nfneg ⊢Ⅎ_x−x∈A⟼B⁡y
33 2 3 32 nfbr ⊢Ⅎx0≤−x∈A⟼B⁡y
34 33 32 2 nfif ⊢Ⅎ_xif0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0
35 nfcv ⊢Ⅎ_yif0≤−x∈A⟼B⁡x−x∈A⟼B⁡x0
36 8 negeqd ⊢y=x→−x∈A⟼B⁡y=−x∈A⟼B⁡x
37 36 breq2d ⊢y=x→0≤−x∈A⟼B⁡y↔0≤−x∈A⟼B⁡x
38 37 36 ifbieq1d ⊢y=x→if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0=if0≤−x∈A⟼B⁡x−x∈A⟼B⁡x0
39 34 35 38 cbvmpt ⊢y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0=x∈A⟼if0≤−x∈A⟼B⁡x−x∈A⟼B⁡x0
40 15 negeqd ⊢φ∧x∈A→−x∈A⟼B⁡x=−B
41 40 breq2d ⊢φ∧x∈A→0≤−x∈A⟼B⁡x↔0≤−B
42 41 40 ifbieq1d ⊢φ∧x∈A→if0≤−x∈A⟼B⁡x−x∈A⟼B⁡x0=if0≤−B−B0
43 42 mpteq2dva ⊢φ→x∈A⟼if0≤−x∈A⟼B⁡x−x∈A⟼B⁡x0=x∈A⟼if0≤−B−B0
44 39 43 eqtrid ⊢φ→y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0=x∈A⟼if0≤−B−B0
45 44 adantr ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0=x∈A⟼if0≤−B−B0
46 23 renegcld ⊢φ∧x∈A⟼B∈MblFn∧y∈A→−x∈A⟼B⁡y∈ℝ
47 23 29 mbfneg ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼−x∈A⟼B⁡y∈MblFn
48 46 47 mbfpos ⊢φ∧x∈A⟼B∈MblFn→y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0∈MblFn
49 45 48 eqeltrrd ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼if0≤−B−B0∈MblFn
50 31 49 jca ⊢φ∧x∈A⟼B∈MblFn→x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn
51 27 adantr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼x∈A⟼B⁡y=x∈A⟼B
52 21 ffvelrnda ⊢φ∧y∈A→x∈A⟼B⁡y∈ℝ
53 52 adantlr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn∧y∈A→x∈A⟼B⁡y∈ℝ
54 19 adantr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0=x∈A⟼if0≤BB0
55 simprl ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→x∈A⟼if0≤BB0∈MblFn
56 54 55 eqeltrd ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼if0≤x∈A⟼B⁡yx∈A⟼B⁡y0∈MblFn
57 44 adantr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0=x∈A⟼if0≤−B−B0
58 simprr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→x∈A⟼if0≤−B−B0∈MblFn
59 57 58 eqeltrd ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼if0≤−x∈A⟼B⁡y−x∈A⟼B⁡y0∈MblFn
60 53 56 59 mbfposr ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→y∈A⟼x∈A⟼B⁡y∈MblFn
61 51 60 eqeltrrd ⊢φ∧x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn→x∈A⟼B∈MblFn
62 50 61 impbida ⊢φ→x∈A⟼B∈MblFn↔x∈A⟼if0≤BB0∈MblFn∧x∈A⟼if0≤−B−B0∈MblFn