Step | Hyp | Ref
| Expression |
1 | | recl 13698 |
. . . . . 6
⊢ (𝐵 ∈ ℂ →
(ℜ‘𝐵) ∈
ℝ) |
2 | 1 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (ℜ‘𝐵) ∈ ℝ) |
3 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) ∧ 𝑥 ∈
𝐴) → 𝑦 ∈
ℝ) |
4 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (𝐴 × {𝑦}) = (𝑥 ∈ 𝐴 ↦ 𝑦) |
5 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → 𝐴 ∈
dom vol) |
6 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (vol‘𝐴) ∈ ℝ) |
7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (vol‘𝐴) ∈ ℝ) |
8 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℝ) |
9 | 8 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℂ) |
10 | | iblconst 23390 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝑦 ∈
ℂ) → (𝐴 ×
{𝑦}) ∈
𝐿1) |
11 | 5, 7, 9, 10 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (𝐴 ×
{𝑦}) ∈
𝐿1) |
12 | 4, 11 | syl5eqelr 2693 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (𝑥 ∈
𝐴 ↦ 𝑦) ∈
𝐿1) |
13 | 3, 12 | itgrevallem1 23367 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → ∫𝐴𝑦 d𝑥 = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0))))) |
14 | | ifan 4084 |
. . . . . . . . . . . 12
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝑦, 𝑦, 0), 0) |
15 | 14 | mpteq2i 4669 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝑦, 𝑦, 0), 0)) |
16 | 15 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝑦, 𝑦, 0), 0))) |
17 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
18 | | ifcl 4080 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
19 | 8, 17, 18 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
20 | | max1 11890 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
21 | 17, 8, 20 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
22 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (if(0
≤ 𝑦, 𝑦, 0) ∈ (0[,)+∞) ↔ (if(0 ≤
𝑦, 𝑦, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑦, 𝑦, 0))) |
23 | 19, 21, 22 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ (0[,)+∞)) |
24 | | itg2const 23313 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ if(0 ≤ 𝑦,
𝑦, 0) ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝑦, 𝑦, 0), 0))) = (if(0 ≤ 𝑦, 𝑦, 0) · (vol‘𝐴))) |
25 | 5, 7, 23, 24 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝑦, 𝑦, 0), 0))) = (if(0 ≤ 𝑦, 𝑦, 0) · (vol‘𝐴))) |
26 | 16, 25 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) = (if(0 ≤ 𝑦, 𝑦, 0) · (vol‘𝐴))) |
27 | | ifan 4084 |
. . . . . . . . . . . 12
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -𝑦, -𝑦, 0), 0) |
28 | 27 | mpteq2i 4669 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝑦, -𝑦, 0), 0)) |
29 | 28 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝑦, -𝑦, 0), 0))) |
30 | | renegcl 10223 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → -𝑦 ∈
ℝ) |
32 | | ifcl 4080 |
. . . . . . . . . . . . 13
⊢ ((-𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝑦, -𝑦, 0) ∈ ℝ) |
33 | 31, 17, 32 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ -𝑦, -𝑦, 0) ∈ ℝ) |
34 | | max1 11890 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ -𝑦
∈ ℝ) → 0 ≤ if(0 ≤ -𝑦, -𝑦, 0)) |
35 | 17, 31, 34 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → 0 ≤ if(0 ≤ -𝑦, -𝑦, 0)) |
36 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (if(0
≤ -𝑦, -𝑦, 0) ∈ (0[,)+∞)
↔ (if(0 ≤ -𝑦,
-𝑦, 0) ∈ ℝ ∧
0 ≤ if(0 ≤ -𝑦, -𝑦, 0))) |
37 | 33, 35, 36 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ -𝑦, -𝑦, 0) ∈ (0[,)+∞)) |
38 | | itg2const 23313 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ if(0 ≤ -𝑦,
-𝑦, 0) ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝑦, -𝑦, 0), 0))) = (if(0 ≤ -𝑦, -𝑦, 0) · (vol‘𝐴))) |
39 | 5, 7, 37, 38 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝑦, -𝑦, 0), 0))) = (if(0 ≤ -𝑦, -𝑦, 0) · (vol‘𝐴))) |
40 | 29, 39 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0))) = (if(0 ≤ -𝑦, -𝑦, 0) · (vol‘𝐴))) |
41 | 26, 40 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0)))) = ((if(0 ≤ 𝑦, 𝑦, 0) · (vol‘𝐴)) − (if(0 ≤ -𝑦, -𝑦, 0) · (vol‘𝐴)))) |
42 | 19 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℂ) |
43 | 33 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → if(0 ≤ -𝑦, -𝑦, 0) ∈ ℂ) |
44 | 6 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (vol‘𝐴) ∈ ℂ) |
45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (vol‘𝐴) ∈ ℂ) |
46 | 42, 43, 45 | subdird 10366 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → ((if(0 ≤ 𝑦, 𝑦, 0) − if(0 ≤ -𝑦, -𝑦, 0)) · (vol‘𝐴)) = ((if(0 ≤ 𝑦, 𝑦, 0) · (vol‘𝐴)) − (if(0 ≤ -𝑦, -𝑦, 0) · (vol‘𝐴)))) |
47 | | max0sub 11901 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (if(0
≤ 𝑦, 𝑦, 0) − if(0 ≤ -𝑦, -𝑦, 0)) = 𝑦) |
48 | 47 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (if(0 ≤ 𝑦, 𝑦, 0) − if(0 ≤ -𝑦, -𝑦, 0)) = 𝑦) |
49 | 48 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → ((if(0 ≤ 𝑦, 𝑦, 0) − if(0 ≤ -𝑦, -𝑦, 0)) · (vol‘𝐴)) = (𝑦 · (vol‘𝐴))) |
50 | 41, 46, 49 | 3eqtr2rd 2651 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → (𝑦 ·
(vol‘𝐴)) =
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝑦), -𝑦, 0))))) |
51 | 13, 50 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑦 ∈
ℝ) → ∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴))) |
52 | 51 | ralrimiva 2949 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∀𝑦
∈ ℝ ∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴))) |
53 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑦 = (ℜ‘𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 = (ℜ‘𝐵)) |
54 | 53 | itgeq2dv 23354 |
. . . . . . 7
⊢ (𝑦 = (ℜ‘𝐵) → ∫𝐴𝑦 d𝑥 = ∫𝐴(ℜ‘𝐵) d𝑥) |
55 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (ℜ‘𝐵) → (𝑦 · (vol‘𝐴)) = ((ℜ‘𝐵) · (vol‘𝐴))) |
56 | 54, 55 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑦 = (ℜ‘𝐵) → (∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴)) ↔ ∫𝐴(ℜ‘𝐵) d𝑥 = ((ℜ‘𝐵) · (vol‘𝐴)))) |
57 | 56 | rspcv 3278 |
. . . . 5
⊢
((ℜ‘𝐵)
∈ ℝ → (∀𝑦 ∈ ℝ ∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴)) → ∫𝐴(ℜ‘𝐵) d𝑥 = ((ℜ‘𝐵) · (vol‘𝐴)))) |
58 | 2, 52, 57 | sylc 63 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∫𝐴(ℜ‘𝐵) d𝑥 = ((ℜ‘𝐵) · (vol‘𝐴))) |
59 | | imcl 13699 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) ∈
ℝ) |
60 | 59 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (ℑ‘𝐵) ∈ ℝ) |
61 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑦 = (ℑ‘𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑦 = (ℑ‘𝐵)) |
62 | 61 | itgeq2dv 23354 |
. . . . . . . . 9
⊢ (𝑦 = (ℑ‘𝐵) → ∫𝐴𝑦 d𝑥 = ∫𝐴(ℑ‘𝐵) d𝑥) |
63 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = (ℑ‘𝐵) → (𝑦 · (vol‘𝐴)) = ((ℑ‘𝐵) · (vol‘𝐴))) |
64 | 62, 63 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑦 = (ℑ‘𝐵) → (∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴)) ↔ ∫𝐴(ℑ‘𝐵) d𝑥 = ((ℑ‘𝐵) · (vol‘𝐴)))) |
65 | 64 | rspcv 3278 |
. . . . . . 7
⊢
((ℑ‘𝐵)
∈ ℝ → (∀𝑦 ∈ ℝ ∫𝐴𝑦 d𝑥 = (𝑦 · (vol‘𝐴)) → ∫𝐴(ℑ‘𝐵) d𝑥 = ((ℑ‘𝐵) · (vol‘𝐴)))) |
66 | 60, 52, 65 | sylc 63 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∫𝐴(ℑ‘𝐵) d𝑥 = ((ℑ‘𝐵) · (vol‘𝐴))) |
67 | 66 | oveq2d 6565 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) = (i · ((ℑ‘𝐵) · (vol‘𝐴)))) |
68 | | ax-icn 9874 |
. . . . . . 7
⊢ i ∈
ℂ |
69 | 68 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → i ∈ ℂ) |
70 | 60 | recnd 9947 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (ℑ‘𝐵) ∈ ℂ) |
71 | 69, 70, 44 | mulassd 9942 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ((i · (ℑ‘𝐵)) · (vol‘𝐴)) = (i · ((ℑ‘𝐵) · (vol‘𝐴)))) |
72 | 67, 71 | eqtr4d 2647 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) = ((i · (ℑ‘𝐵)) · (vol‘𝐴))) |
73 | 58, 72 | oveq12d 6567 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (((ℜ‘𝐵) · (vol‘𝐴)) + ((i · (ℑ‘𝐵)) · (vol‘𝐴)))) |
74 | 2 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (ℜ‘𝐵) ∈ ℂ) |
75 | | mulcl 9899 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
76 | 68, 70, 75 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (i · (ℑ‘𝐵)) ∈ ℂ) |
77 | 74, 76, 44 | adddird 9944 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (((ℜ‘𝐵) + (i · (ℑ‘𝐵))) · (vol‘𝐴)) = (((ℜ‘𝐵) · (vol‘𝐴)) + ((i ·
(ℑ‘𝐵)) ·
(vol‘𝐴)))) |
78 | 73, 77 | eqtr4d 2647 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (((ℜ‘𝐵) + (i · (ℑ‘𝐵))) · (vol‘𝐴))) |
79 | | simpl3 1059 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) ∧ 𝑥 ∈
𝐴) → 𝐵 ∈ ℂ) |
80 | | fconstmpt 5085 |
. . . 4
⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
81 | | iblconst 23390 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝐴 ×
{𝐵}) ∈
𝐿1) |
82 | 80, 81 | syl5eqelr 2693 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝑥 ∈
𝐴 ↦ 𝐵) ∈
𝐿1) |
83 | 79, 82 | itgcnval 23372 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) |
84 | | replim 13704 |
. . . 4
⊢ (𝐵 ∈ ℂ → 𝐵 = ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) |
85 | 84 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → 𝐵 =
((ℜ‘𝐵) + (i
· (ℑ‘𝐵)))) |
86 | 85 | oveq1d 6564 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → (𝐵 ·
(vol‘𝐴)) =
(((ℜ‘𝐵) + (i
· (ℑ‘𝐵))) · (vol‘𝐴))) |
87 | 78, 83, 86 | 3eqtr4d 2654 |
1
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
ℂ) → ∫𝐴𝐵 d𝑥 = (𝐵 · (vol‘𝐴))) |