Metamath Proof Explorer

Theorem ibladd

Description: Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itgadd.1 ⊢φ∧x∈A→B∈V
itgadd.2 ⊢φ→x∈A⟼B∈𝐿1
itgadd.3 ⊢φ∧x∈A→C∈V
itgadd.4 ⊢φ→x∈A⟼C∈𝐿1
Assertion ibladd ⊢φ→x∈A⟼B+C∈𝐿1

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢φ∧x∈A→B∈V
2 itgadd.2 ⊢φ→x∈A⟼B∈𝐿1
3 itgadd.3 ⊢φ∧x∈A→C∈V
4 itgadd.4 ⊢φ→x∈A⟼C∈𝐿1
5 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
6 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
7 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
8 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
9 5 6 7 8 1 iblcnlem ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
10 2 9 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
11 10 simp1d ⊢φ→x∈A⟼B∈MblFn
12 11 1 mbfdm2 ⊢φ→A∈dom⁡vol
13 eqidd ⊢φ→x∈A⟼B=x∈A⟼B
14 eqidd ⊢φ→x∈A⟼C=x∈A⟼C
15 12 1 3 13 14 offval2 ⊢φ→x∈A⟼B+fx∈A⟼C=x∈A⟼B+C
16 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0
17 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0
18 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0
19 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0
20 16 17 18 19 3 iblcnlem ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
21 4 20 mpbid ⊢φ→x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
22 21 simp1d ⊢φ→x∈A⟼C∈MblFn
23 11 22 mbfadd ⊢φ→x∈A⟼B+fx∈A⟼C∈MblFn
24 15 23 eqeltrrd ⊢φ→x∈A⟼B+C∈MblFn
25 11 1 mbfmptcl ⊢φ∧x∈A→B∈ℂ
26 25 recld ⊢φ∧x∈A→ℜ⁡B∈ℝ
27 22 3 mbfmptcl ⊢φ∧x∈A→C∈ℂ
28 27 recld ⊢φ∧x∈A→ℜ⁡C∈ℝ
29 25 27 readdd ⊢φ∧x∈A→ℜ⁡B+C=ℜ⁡B+ℜ⁡C
30 25 ismbfcn2 ⊢φ→x∈A⟼B∈MblFn↔x∈A⟼ℜ⁡B∈MblFn∧x∈A⟼ℑ⁡B∈MblFn
31 11 30 mpbid ⊢φ→x∈A⟼ℜ⁡B∈MblFn∧x∈A⟼ℑ⁡B∈MblFn
32 31 simpld ⊢φ→x∈A⟼ℜ⁡B∈MblFn
33 27 ismbfcn2 ⊢φ→x∈A⟼C∈MblFn↔x∈A⟼ℜ⁡C∈MblFn∧x∈A⟼ℑ⁡C∈MblFn
34 22 33 mpbid ⊢φ→x∈A⟼ℜ⁡C∈MblFn∧x∈A⟼ℑ⁡C∈MblFn
35 34 simpld ⊢φ→x∈A⟼ℜ⁡C∈MblFn
36 10 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ
37 36 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ
38 21 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ
39 38 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ
40 26 28 29 32 35 37 39 ibladdlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0∈ℝ
41 26 renegcld ⊢φ∧x∈A→−ℜ⁡B∈ℝ
42 28 renegcld ⊢φ∧x∈A→−ℜ⁡C∈ℝ
43 29 negeqd ⊢φ∧x∈A→−ℜ⁡B+C=−ℜ⁡B+ℜ⁡C
44 26 recnd ⊢φ∧x∈A→ℜ⁡B∈ℂ
45 28 recnd ⊢φ∧x∈A→ℜ⁡C∈ℂ
46 44 45 negdid ⊢φ∧x∈A→−ℜ⁡B+ℜ⁡C=-ℜ⁡B+−ℜ⁡C
47 43 46 eqtrd ⊢φ∧x∈A→−ℜ⁡B+C=-ℜ⁡B+−ℜ⁡C
48 26 32 mbfneg ⊢φ→x∈A⟼−ℜ⁡B∈MblFn
49 28 35 mbfneg ⊢φ→x∈A⟼−ℜ⁡C∈MblFn
50 36 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ
51 38 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ
52 41 42 47 48 49 50 51 ibladdlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0∈ℝ
53 40 52 jca ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0∈ℝ
54 25 imcld ⊢φ∧x∈A→ℑ⁡B∈ℝ
55 27 imcld ⊢φ∧x∈A→ℑ⁡C∈ℝ
56 25 27 imaddd ⊢φ∧x∈A→ℑ⁡B+C=ℑ⁡B+ℑ⁡C
57 31 simprd ⊢φ→x∈A⟼ℑ⁡B∈MblFn
58 34 simprd ⊢φ→x∈A⟼ℑ⁡C∈MblFn
59 10 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
60 59 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ
61 21 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
62 61 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ
63 54 55 56 57 58 60 62 ibladdlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0∈ℝ
64 54 renegcld ⊢φ∧x∈A→−ℑ⁡B∈ℝ
65 55 renegcld ⊢φ∧x∈A→−ℑ⁡C∈ℝ
66 56 negeqd ⊢φ∧x∈A→−ℑ⁡B+C=−ℑ⁡B+ℑ⁡C
67 54 recnd ⊢φ∧x∈A→ℑ⁡B∈ℂ
68 55 recnd ⊢φ∧x∈A→ℑ⁡C∈ℂ
69 67 68 negdid ⊢φ∧x∈A→−ℑ⁡B+ℑ⁡C=-ℑ⁡B+−ℑ⁡C
70 66 69 eqtrd ⊢φ∧x∈A→−ℑ⁡B+C=-ℑ⁡B+−ℑ⁡C
71 54 57 mbfneg ⊢φ→x∈A⟼−ℑ⁡B∈MblFn
72 55 58 mbfneg ⊢φ→x∈A⟼−ℑ⁡C∈MblFn
73 59 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
74 61 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
75 64 65 70 71 72 73 74 ibladdlem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0∈ℝ
76 63 75 jca ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0∈ℝ
77 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0
78 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0
79 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0
80 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0
81 ovexd ⊢φ∧x∈A→B+C∈V
82 77 78 79 80 81 iblcnlem ⊢φ→x∈A⟼B+C∈𝐿1↔x∈A⟼B+C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0∈ℝ
83 24 53 76 82 mpbir3and ⊢φ→x∈A⟼B+C∈𝐿1