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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgcnval.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion iblneg ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ 𝐿1 )

Proof

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