Metamath Proof Explorer

Theorem ibladdnc

Description: Choice-free analogue of itgadd . A measurability hypothesis is necessitated by the loss of mbfadd ; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017)

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

Proof

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