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 ‘ 𝐴 ) ) )