Metamath Proof Explorer

Theorem iblneg

Description: The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 ⊢ φ ∧ x ∈ A → B ∈ V
itgcnval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
Assertion iblneg ⊢ φ → x ∈ A ⟼ − B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 itgcnval.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgcnval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
4 2 3 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
5 4 1 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
6 5 renegd ⊢ φ ∧ x ∈ A → ℜ ⁡ − B = − ℜ ⁡ B
7 6 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ − B ↔ 0 ≤ − ℜ ⁡ B
8 7 6 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 = if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
9 8 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 = x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
10 5 iblcn ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
11 2 10 mpbid ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
12 11 simpld ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1
13 5 recld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
14 13 iblre ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
15 12 14 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
16 15 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
17 9 16 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 ∈ 𝐿 1
18 6 negeqd ⊢ φ ∧ x ∈ A → − ℜ ⁡ − B = − − ℜ ⁡ B
19 13 recnd ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℂ
20 19 negnegd ⊢ φ ∧ x ∈ A → − − ℜ ⁡ B = ℜ ⁡ B
21 18 20 eqtrd ⊢ φ ∧ x ∈ A → − ℜ ⁡ − B = ℜ ⁡ B
22 21 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ − ℜ ⁡ − B ↔ 0 ≤ ℜ ⁡ B
23 22 21 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 = if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
24 23 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 = x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
25 15 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1
26 24 25 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 ∈ 𝐿 1
27 5 negcld ⊢ φ ∧ x ∈ A → − B ∈ ℂ
28 27 recld ⊢ φ ∧ x ∈ A → ℜ ⁡ − B ∈ ℝ
29 28 iblre ⊢ φ → x ∈ A ⟼ ℜ ⁡ − B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 ∈ 𝐿 1
30 17 26 29 mpbir2and ⊢ φ → x ∈ A ⟼ ℜ ⁡ − B ∈ 𝐿 1
31 5 imnegd ⊢ φ ∧ x ∈ A → ℑ ⁡ − B = − ℑ ⁡ B
32 31 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ ℑ ⁡ − B ↔ 0 ≤ − ℑ ⁡ B
33 32 31 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 = if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
34 33 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 = x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
35 11 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
36 5 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
37 36 iblre ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
38 35 37 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
39 38 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
40 34 39 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 ∈ 𝐿 1
41 31 negeqd ⊢ φ ∧ x ∈ A → − ℑ ⁡ − B = − − ℑ ⁡ B
42 36 recnd ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℂ
43 42 negnegd ⊢ φ ∧ x ∈ A → − − ℑ ⁡ B = ℑ ⁡ B
44 41 43 eqtrd ⊢ φ ∧ x ∈ A → − ℑ ⁡ − B = ℑ ⁡ B
45 44 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ − ℑ ⁡ − B ↔ 0 ≤ ℑ ⁡ B
46 45 44 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 = if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
47 46 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 = x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
48 38 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1
49 47 48 eqeltrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 ∈ 𝐿 1
50 27 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ − B ∈ ℝ
51 50 iblre ⊢ φ → x ∈ A ⟼ ℑ ⁡ − B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 ∈ 𝐿 1
52 40 49 51 mpbir2and ⊢ φ → x ∈ A ⟼ ℑ ⁡ − B ∈ 𝐿 1
53 27 iblcn ⊢ φ → x ∈ A ⟼ − B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ − B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ − B ∈ 𝐿 1
54 30 52 53 mpbir2and ⊢ φ → x ∈ A ⟼ − B ∈ 𝐿 1