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

Metamath Proof Explorer

Theorem itgconst

Description: Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion itgconst ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∫ 𝐴 𝐵 d 𝑥 = ( 𝐵 · ( vol ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑦 = ( ℜ ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 = ( ℜ ‘ 𝐵 ) )
2 1 itgeq2dv ⊢ ( 𝑦 = ( ℜ ‘ 𝐵 ) → ∫ 𝐴 𝑦 d 𝑥 = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 )
3 oveq1 ⊢ ( 𝑦 = ( ℜ ‘ 𝐵 ) → ( 𝑦 · ( vol ‘ 𝐴 ) ) = ( ( ℜ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) )
4 2 3 eqeq12d ⊢ ( 𝑦 = ( ℜ ‘ 𝐵 ) → ( ∫ 𝐴 𝑦 d 𝑥 = ( 𝑦 · ( vol ‘ 𝐴 ) ) ↔ ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 = ( ( ℜ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) ) )
5 simplr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
6 fconstmpt ⊢ ( 𝐴 × { 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝑦 )
7 simpl1 ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ dom vol )
8 simp2 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( vol ‘ 𝐴 ) ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( vol ‘ 𝐴 ) ∈ ℝ )
10 simpr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
11 10 recnd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
12 iblconst ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 × { 𝑦 } ) ∈ 𝐿1 )
13 7 9 11 12 syl3anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐴 × { 𝑦 } ) ∈ 𝐿1 )
14 6 13 eqeltrrid ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑦 ) ∈ 𝐿1 )
15 5 14 itgrevallem1 ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ∫ 𝐴 𝑦 d 𝑥 = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) ) ) )
16 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝑦 , 𝑦 , 0 ) , 0 )
17 16 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝑦 , 𝑦 , 0 ) , 0 ) )
18 17 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝑦 , 𝑦 , 0 ) , 0 ) ) )
19 0re ⊢ 0 ∈ ℝ
20 ifcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
21 10 19 20 sylancl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ )
22 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
23 19 10 22 sylancr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) )
24 elrege0 ⊢ ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ) )
25 21 23 24 sylanbrc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) )
26 itg2const ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝑦 , 𝑦 , 0 ) , 0 ) ) ) = ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
27 7 9 25 26 syl3anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ 𝑦 , 𝑦 , 0 ) , 0 ) ) ) = ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
28 18 27 eqtrid ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) = ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
29 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) , 0 )
30 29 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) , 0 ) )
31 30 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) , 0 ) ) )
32 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
33 32 adantl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → - 𝑦 ∈ ℝ )
34 ifcl ⊢ ( ( - 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ℝ )
35 33 19 34 sylancl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ℝ )
36 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) )
37 19 33 36 sylancr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) )
38 elrege0 ⊢ ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ) )
39 35 37 38 sylanbrc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) )
40 itg2const ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) , 0 ) ) ) = ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
41 7 9 39 40 syl3anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) , 0 ) ) ) = ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
42 31 41 eqtrid ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) ) = ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) )
43 28 42 oveq12d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) ) ) = ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) − ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) ) )
44 21 recnd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ 𝑦 , 𝑦 , 0 ) ∈ ℂ )
45 35 recnd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ∈ ℂ )
46 8 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( vol ‘ 𝐴 ) ∈ ℂ )
47 46 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( vol ‘ 𝐴 ) ∈ ℂ )
48 44 45 47 subdird ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) − if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ) · ( vol ‘ 𝐴 ) ) = ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) − ( if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) · ( vol ‘ 𝐴 ) ) ) )
49 max0sub ⊢ ( 𝑦 ∈ ℝ → ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) − if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ) = 𝑦 )
50 49 adantl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) − if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ) = 𝑦 )
51 50 oveq1d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( ( if ( 0 ≤ 𝑦 , 𝑦 , 0 ) − if ( 0 ≤ - 𝑦 , - 𝑦 , 0 ) ) · ( vol ‘ 𝐴 ) ) = ( 𝑦 · ( vol ‘ 𝐴 ) ) )
52 43 48 51 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 · ( vol ‘ 𝐴 ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝑦 ) , - 𝑦 , 0 ) ) ) ) )
53 15 52 eqtr4d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ ) → ∫ 𝐴 𝑦 d 𝑥 = ( 𝑦 · ( vol ‘ 𝐴 ) ) )
54 53 ralrimiva ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∀ 𝑦 ∈ ℝ ∫ 𝐴 𝑦 d 𝑥 = ( 𝑦 · ( vol ‘ 𝐴 ) ) )
55 recl ⊢ ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
56 55 3ad2ant3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
57 4 54 56 rspcdva ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 = ( ( ℜ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) )
58 simpl ⊢ ( ( 𝑦 = ( ℑ ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 = ( ℑ ‘ 𝐵 ) )
59 58 itgeq2dv ⊢ ( 𝑦 = ( ℑ ‘ 𝐵 ) → ∫ 𝐴 𝑦 d 𝑥 = ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 )
60 oveq1 ⊢ ( 𝑦 = ( ℑ ‘ 𝐵 ) → ( 𝑦 · ( vol ‘ 𝐴 ) ) = ( ( ℑ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) )
61 59 60 eqeq12d ⊢ ( 𝑦 = ( ℑ ‘ 𝐵 ) → ( ∫ 𝐴 𝑦 d 𝑥 = ( 𝑦 · ( vol ‘ 𝐴 ) ) ↔ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 = ( ( ℑ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) ) )
62 imcl ⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℝ )
63 62 3ad2ant3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
64 61 54 63 rspcdva ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 = ( ( ℑ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) )
65 64 oveq2d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ( i · ( ( ℑ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) ) )
66 ax-icn ⊢ i ∈ ℂ
67 66 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → i ∈ ℂ )
68 63 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
69 67 68 46 mulassd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ℑ ‘ 𝐵 ) ) · ( vol ‘ 𝐴 ) ) = ( i · ( ( ℑ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) ) )
70 65 69 eqtr4d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ( ( i · ( ℑ ‘ 𝐵 ) ) · ( vol ‘ 𝐴 ) ) )
71 57 70 oveq12d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( ( ( ℜ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) + ( ( i · ( ℑ ‘ 𝐵 ) ) · ( vol ‘ 𝐴 ) ) ) )
72 56 recnd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
73 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
74 66 68 73 sylancr ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
75 72 74 46 adddird ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) · ( vol ‘ 𝐴 ) ) = ( ( ( ℜ ‘ 𝐵 ) · ( vol ‘ 𝐴 ) ) + ( ( i · ( ℑ ‘ 𝐵 ) ) · ( vol ‘ 𝐴 ) ) ) )
76 71 75 eqtr4d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) · ( vol ‘ 𝐴 ) ) )
77 simpl3 ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
78 fconstmpt ⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
79 iblconst ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ 𝐿1 )
80 78 79 eqeltrrid ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
81 77 80 itgcnval ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
82 replim ⊢ ( 𝐵 ∈ ℂ → 𝐵 = ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
83 82 3ad2ant3 ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → 𝐵 = ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
84 83 oveq1d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · ( vol ‘ 𝐴 ) ) = ( ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) · ( vol ‘ 𝐴 ) ) )
85 76 81 84 3eqtr4d ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∫ 𝐴 𝐵 d 𝑥 = ( 𝐵 · ( vol ‘ 𝐴 ) ) )