This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgadd

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

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

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6 2 5 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7 6 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
9 4 8 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10 9 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
11 7 10 readdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
12 11 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 )
13 7 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
14 7 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
15 2 14 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
17 10 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
18 10 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) ) )
19 4 18 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) )
20 19 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 )
21 13 16 17 20 13 17 itgaddlem2 ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
22 12 21 eqtrd ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
23 7 10 imaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
24 23 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 )
25 7 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
26 15 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
27 10 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
28 19 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 )
29 25 26 27 28 25 27 itgaddlem2 ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
30 24 29 eqtrd ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
31 30 oveq2d ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
32 ax-icn ⊢ i ∈ ℂ
33 32 a1i ⊢ ( 𝜑 → i ∈ ℂ )
34 25 26 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
35 27 28 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
36 33 34 35 adddid ⊢ ( 𝜑 → ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
37 31 36 eqtrd ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
38 22 37 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
39 13 16 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
40 17 20 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
41 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
42 32 34 41 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
43 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
44 32 35 43 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
45 39 40 42 44 add4d ⊢ ( 𝜑 → ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
46 38 45 eqtrd ⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
47 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ V )
48 1 2 3 4 ibladd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )
49 47 48 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) )
50 1 2 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
51 3 4 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
52 50 51 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
53 46 49 52 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )