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 ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 nfcv ⊢ Ⅎ _ x 0
3 nfcv ⊢ Ⅎ _ x ≤
4 nffvmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B ⁡ y
5 2 3 4 nfbr ⊢ Ⅎ x 0 ≤ x ∈ A ⟼ B ⁡ y
6 5 4 2 nfif ⊢ Ⅎ _ x if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0
7 nfcv ⊢ Ⅎ _ y if 0 ≤ x ∈ A ⟼ B ⁡ x x ∈ A ⟼ B ⁡ x 0
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 → if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 = if 0 ≤ x ∈ A ⟼ B ⁡ x x ∈ A ⟼ B ⁡ x 0
11 6 7 10 cbvmpt ⊢ y ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ x x ∈ A ⟼ B ⁡ x 0
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 → if 0 ≤ x ∈ A ⟼ B ⁡ x x ∈ A ⟼ B ⁡ x 0 = if 0 ≤ B B 0
18 17 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ x x ∈ A ⟼ B ⁡ x 0 = x ∈ A ⟼ if 0 ≤ B B 0
19 11 18 eqtrid ⊢ φ → y ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ B B 0
20 19 adantr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → y ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ B B 0
21 1 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℝ
22 21 adantr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ B : A ⟶ ℝ
23 22 ffvelcdmda ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn ∧ y ∈ A → x ∈ A ⟼ B ⁡ y ∈ ℝ
24 nfcv ⊢ Ⅎ _ y x ∈ 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 ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 ∈ MblFn
31 20 30 eqeltrrd ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
32 4 nfneg ⊢ Ⅎ _ x − x ∈ A ⟼ B ⁡ y
33 2 3 32 nfbr ⊢ Ⅎ x 0 ≤ − x ∈ A ⟼ B ⁡ y
34 33 32 2 nfif ⊢ Ⅎ _ x if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0
35 nfcv ⊢ Ⅎ _ y if 0 ≤ − x ∈ A ⟼ B ⁡ x − x ∈ A ⟼ B ⁡ x 0
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 → if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 = if 0 ≤ − x ∈ A ⟼ B ⁡ x − x ∈ A ⟼ B ⁡ x 0
39 34 35 38 cbvmpt ⊢ y ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ x − x ∈ A ⟼ B ⁡ x 0
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 → if 0 ≤ − x ∈ A ⟼ B ⁡ x − x ∈ A ⟼ B ⁡ x 0 = if 0 ≤ − B − B 0
43 42 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ x − x ∈ A ⟼ B ⁡ x 0 = x ∈ A ⟼ if 0 ≤ − B − B 0
44 39 43 eqtrid ⊢ φ → y ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ − B − B 0
45 44 adantr ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → y ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ − B − B 0
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 ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 ∈ MblFn
49 45 48 eqeltrrd ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
50 31 49 jca ⊢ φ ∧ x ∈ A ⟼ B ∈ MblFn → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
51 27 adantr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ x ∈ A ⟼ B ⁡ y = x ∈ A ⟼ B
52 21 ffvelcdmda ⊢ φ ∧ y ∈ A → x ∈ A ⟼ B ⁡ y ∈ ℝ
53 52 adantlr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn ∧ y ∈ A → x ∈ A ⟼ B ⁡ y ∈ ℝ
54 19 adantr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ B B 0
55 simprl ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
56 54 55 eqeltrd ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ if 0 ≤ x ∈ A ⟼ B ⁡ y x ∈ A ⟼ B ⁡ y 0 ∈ MblFn
57 44 adantr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 = x ∈ A ⟼ if 0 ≤ − B − B 0
58 simprr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
59 57 58 eqeltrd ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ if 0 ≤ − x ∈ A ⟼ B ⁡ y − x ∈ A ⟼ B ⁡ y 0 ∈ MblFn
60 53 56 59 mbfposr ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → y ∈ A ⟼ x ∈ A ⟼ B ⁡ y ∈ MblFn
61 51 60 eqeltrrd ⊢ φ ∧ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn → x ∈ A ⟼ B ∈ MblFn
62 50 61 impbida ⊢ φ → x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn