Metamath Proof Explorer

Theorem itgaddnc

Description: Choice-free analogue of itgadd . (Contributed by Brendan Leahy, 11-Nov-2017)

Ref Expression
Hypotheses ibladdnc.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
ibladdnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
ibladdnc.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
ibladdnc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
ibladdnc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
Assertion itgaddnc ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ibladdnc.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 ibladdnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 ibladdnc.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 ibladdnc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 ibladdnc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
6 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7 2 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8 7 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10 4 9 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
11 10 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12 8 11 readdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
13 12 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 )
14 8 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
15 8 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
16 2 15 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
17 16 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
18 11 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
19 11 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) ) )
20 4 19 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) )
21 20 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 )
22 8 11 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
23 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) )
24 ref ⊢ ℜ : ℂ ⟶ ℝ
25 24 a1i ⊢ ( 𝜑 → ℜ : ℂ ⟶ ℝ )
26 25 feqmptd ⊢ ( 𝜑 → ℜ = ( 𝑦 ∈ ℂ ↦ ( ℜ ‘ 𝑦 ) ) )
27 fveq2 ⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( ℜ ‘ 𝑦 ) = ( ℜ ‘ ( 𝐵 + 𝐶 ) ) )
28 22 23 26 27 fmptco ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) )
29 12 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) )
30 28 29 eqtrd ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) )
31 22 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) : 𝐴 ⟶ ℂ )
32 ismbfcn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) ) )
33 31 32 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) ) )
34 5 33 mpbid ⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) )
35 34 simpld ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn )
36 30 35 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) ∈ MblFn )
37 14 17 18 21 36 14 18 itgaddnclem2 ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
38 13 37 eqtrd ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
39 8 11 imaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
40 39 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 )
41 8 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
42 16 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
43 11 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
44 20 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 )
45 imf ⊢ ℑ : ℂ ⟶ ℝ
46 45 a1i ⊢ ( 𝜑 → ℑ : ℂ ⟶ ℝ )
47 46 feqmptd ⊢ ( 𝜑 → ℑ = ( 𝑦 ∈ ℂ ↦ ( ℑ ‘ 𝑦 ) ) )
48 fveq2 ⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( ℑ ‘ 𝑦 ) = ( ℑ ‘ ( 𝐵 + 𝐶 ) ) )
49 22 23 47 48 fmptco ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) )
50 39 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) )
51 49 50 eqtrd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) )
52 34 simprd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn )
53 51 52 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) ∈ MblFn )
54 41 42 43 44 53 41 43 itgaddnclem2 ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
55 40 54 eqtrd ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
56 55 oveq2d ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
57 ax-icn ⊢ i ∈ ℂ
58 57 a1i ⊢ ( 𝜑 → i ∈ ℂ )
59 41 42 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
60 43 44 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
61 58 59 60 adddid ⊢ ( 𝜑 → ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
62 56 61 eqtrd ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
63 38 62 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
64 14 17 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
65 18 21 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
66 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
67 57 59 66 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
68 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
69 57 60 68 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
70 64 65 67 69 add4d ⊢ ( 𝜑 → ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
71 63 70 eqtrd ⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
72 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ V )
73 1 2 3 4 5 ibladdnc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )
74 72 73 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) )
75 1 2 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
76 3 4 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
77 75 76 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
78 71 74 77 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )