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∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
19 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
20 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
21 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
22 18 19 20 21 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∈ℝ
23 2 22 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∈ℝ
24 23 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ
25 24 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0∈ℝ
26 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0
27 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0
28 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0
29 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0
30 26 27 28 29 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∈ℝ
31 4 30 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∈ℝ
32 31 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ
33 32 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Cℜ⁡C0∈ℝ
34 9 13 14 17 25 33 ibladdnclem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0∈ℝ
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∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0∈ℝ
44 32 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡C−ℜ⁡C0∈ℝ
45 35 36 41 42 43 44 ibladdnclem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0∈ℝ
46 34 45 jca ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0∈ℝ
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∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
52 51 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0∈ℝ
53 31 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
54 53 simpld ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Cℑ⁡C0∈ℝ
55 47 48 49 50 52 54 ibladdnclem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0∈ℝ
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∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0∈ℝ
65 53 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡C−ℑ⁡C0∈ℝ
66 56 57 62 63 64 65 ibladdnclem ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0∈ℝ
67 55 66 jca ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0∈ℝ
68 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡B+Cℜ⁡B+C0
69 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B+C−ℜ⁡B+C0
70 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡B+Cℑ⁡B+C0
71 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B+C−ℑ⁡B+C0
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∈ℝ⟼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∈ℝ
74 5 46 67 73 mpbir3and ⊢φ→x∈A⟼B+C∈𝐿1