Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgmulc2nc Structured version   Visualization version   GIF version

Theorem itgmulc2nc 35439
 Description: Choice-free analogue of itgmulc2 24546. (Contributed by Brendan Leahy, 19-Nov-2017.)
Hypotheses
Ref Expression
itgmulc2nc.1 (𝜑𝐶 ∈ ℂ)
itgmulc2nc.2 ((𝜑𝑥𝐴) → 𝐵𝑉)
itgmulc2nc.3 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
itgmulc2nc.m (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
Assertion
Ref Expression
itgmulc2nc (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥   𝑥,𝑉
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem itgmulc2nc
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 itgmulc2nc.1 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
21recld 14614 . . . . . . . 8 (𝜑 → (ℜ‘𝐶) ∈ ℝ)
32recnd 10720 . . . . . . 7 (𝜑 → (ℜ‘𝐶) ∈ ℂ)
43adantr 484 . . . . . 6 ((𝜑𝑥𝐴) → (ℜ‘𝐶) ∈ ℂ)
5 itgmulc2nc.3 . . . . . . . . . 10 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
6 iblmbf 24480 . . . . . . . . . 10 ((𝑥𝐴𝐵) ∈ 𝐿1 → (𝑥𝐴𝐵) ∈ MblFn)
75, 6syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
8 itgmulc2nc.2 . . . . . . . . 9 ((𝜑𝑥𝐴) → 𝐵𝑉)
97, 8mbfmptcl 24349 . . . . . . . 8 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
109recld 14614 . . . . . . 7 ((𝜑𝑥𝐴) → (ℜ‘𝐵) ∈ ℝ)
1110recnd 10720 . . . . . 6 ((𝜑𝑥𝐴) → (ℜ‘𝐵) ∈ ℂ)
124, 11mulcld 10712 . . . . 5 ((𝜑𝑥𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
139iblcn 24511 . . . . . . . 8 (𝜑 → ((𝑥𝐴𝐵) ∈ 𝐿1 ↔ ((𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
145, 13mpbid 235 . . . . . . 7 (𝜑 → ((𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))
1514simpld 498 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1)
16 itgmulc2nc.m . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
17 ovexd 7191 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐶 · 𝐵) ∈ V)
1816, 17mbfdm2 24350 . . . . . . . 8 (𝜑𝐴 ∈ dom vol)
19 fconstmpt 5588 . . . . . . . . 9 (𝐴 × {(ℜ‘𝐶)}) = (𝑥𝐴 ↦ (ℜ‘𝐶))
2019a1i 11 . . . . . . . 8 (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥𝐴 ↦ (ℜ‘𝐶)))
21 eqidd 2759 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐵)) = (𝑥𝐴 ↦ (ℜ‘𝐵)))
2218, 4, 10, 20, 21offval2 7430 . . . . . . 7 (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℜ‘𝐵))) = (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))))
23 iblmbf 24480 . . . . . . . . 9 ((𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 → (𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
2415, 23syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
2511fmpttd 6876 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ)
2624, 2, 25mbfmulc2re 24361 . . . . . . 7 (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
2722, 26eqeltrrd 2853 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
283, 10, 15, 27iblmulc2nc 35436 . . . . 5 (𝜑 → (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
2912, 28itgcl 24496 . . . 4 (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
30 ax-icn 10647 . . . . 5 i ∈ ℂ
319imcld 14615 . . . . . . . 8 ((𝜑𝑥𝐴) → (ℑ‘𝐵) ∈ ℝ)
3231recnd 10720 . . . . . . 7 ((𝜑𝑥𝐴) → (ℑ‘𝐵) ∈ ℂ)
334, 32mulcld 10712 . . . . . 6 ((𝜑𝑥𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
3414simprd 499 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)
35 eqidd 2759 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐵)) = (𝑥𝐴 ↦ (ℑ‘𝐵)))
3618, 4, 31, 20, 35offval2 7430 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) = (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))))
37 iblmbf 24480 . . . . . . . . . 10 ((𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 → (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
3834, 37syl 17 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
3932fmpttd 6876 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ)
4038, 2, 39mbfmulc2re 24361 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
4136, 40eqeltrrd 2853 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
423, 31, 34, 41iblmulc2nc 35436 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
4333, 42itgcl 24496 . . . . 5 (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
44 mulcl 10672 . . . . 5 ((i ∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
4530, 43, 44sylancr 590 . . . 4 (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
461imcld 14615 . . . . . . . . 9 (𝜑 → (ℑ‘𝐶) ∈ ℝ)
4746recnd 10720 . . . . . . . 8 (𝜑 → (ℑ‘𝐶) ∈ ℂ)
4847negcld 11035 . . . . . . 7 (𝜑 → -(ℑ‘𝐶) ∈ ℂ)
4948adantr 484 . . . . . 6 ((𝜑𝑥𝐴) → -(ℑ‘𝐶) ∈ ℂ)
5049, 32mulcld 10712 . . . . 5 ((𝜑𝑥𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
51 fconstmpt 5588 . . . . . . . . 9 (𝐴 × {-(ℑ‘𝐶)}) = (𝑥𝐴 ↦ -(ℑ‘𝐶))
5251a1i 11 . . . . . . . 8 (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥𝐴 ↦ -(ℑ‘𝐶)))
5318, 49, 31, 52, 35offval2 7430 . . . . . . 7 (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) = (𝑥𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))))
5446renegcld 11118 . . . . . . . 8 (𝜑 → -(ℑ‘𝐶) ∈ ℝ)
5538, 54, 39mbfmulc2re 24361 . . . . . . 7 (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
5653, 55eqeltrrd 2853 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
5748, 31, 34, 56iblmulc2nc 35436 . . . . 5 (𝜑 → (𝑥𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
5850, 57itgcl 24496 . . . 4 (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
5947adantr 484 . . . . . . 7 ((𝜑𝑥𝐴) → (ℑ‘𝐶) ∈ ℂ)
6059, 11mulcld 10712 . . . . . 6 ((𝜑𝑥𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
61 fconstmpt 5588 . . . . . . . . . 10 (𝐴 × {(ℑ‘𝐶)}) = (𝑥𝐴 ↦ (ℑ‘𝐶))
6261a1i 11 . . . . . . . . 9 (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥𝐴 ↦ (ℑ‘𝐶)))
6318, 59, 10, 62, 21offval2 7430 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℜ‘𝐵))) = (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))))
6424, 46, 25mbfmulc2re 24361 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
6563, 64eqeltrrd 2853 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
6647, 10, 15, 65iblmulc2nc 35436 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
6760, 66itgcl 24496 . . . . 5 (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
68 mulcl 10672 . . . . 5 ((i ∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
6930, 67, 68sylancr 590 . . . 4 (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
7029, 45, 58, 69add4d 10919 . . 3 (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
7130a1i 11 . . . . . 6 (𝜑 → i ∈ ℂ)
7271, 47mulcld 10712 . . . . 5 (𝜑 → (i · (ℑ‘𝐶)) ∈ ℂ)
738, 5itgcl 24496 . . . . 5 (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
743, 72, 73adddird 10717 . . . 4 (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)))
758, 5itgcnval 24512 . . . . . . 7 (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
7675oveq2d 7172 . . . . . 6 (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
7710, 15itgcl 24496 . . . . . . 7 (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ)
7831, 34itgcl 24496 . . . . . . . 8 (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ)
79 mulcl 10672 . . . . . . . 8 ((i ∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
8030, 78, 79sylancr 590 . . . . . . 7 (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
813, 77, 80adddid 10716 . . . . . 6 (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
823, 10, 15, 27, 2, 10itgmulc2nclem2 35438 . . . . . . 7 (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥)
833, 71, 78mul12d 10900 . . . . . . . 8 (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
843, 31, 34, 41, 2, 31itgmulc2nclem2 35438 . . . . . . . . 9 (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)
8584oveq2d 7172 . . . . . . . 8 (𝜑 → (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
8683, 85eqtrd 2793 . . . . . . 7 (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
8782, 86oveq12d 7174 . . . . . 6 (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
8876, 81, 873eqtrd 2797 . . . . 5 (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
8975oveq2d 7172 . . . . . 6 (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
9072, 77, 80adddid 10716 . . . . . 6 (𝜑 → ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
9171, 47, 77mulassd 10715 . . . . . . . . 9 (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)))
9247, 10, 15, 65, 46, 10itgmulc2nclem2 35438 . . . . . . . . . 10 (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)
9392oveq2d 7172 . . . . . . . . 9 (𝜑 → (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
9491, 93eqtrd 2793 . . . . . . . 8 (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
9571, 47, 71, 78mul4d 10903 . . . . . . . . 9 (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
96 ixi 11320 . . . . . . . . . . 11 (i · i) = -1
9796oveq1i 7166 . . . . . . . . . 10 ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
9847, 78mulcld 10712 . . . . . . . . . . 11 (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
9998mulm1d 11143 . . . . . . . . . 10 (𝜑 → (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
10097, 99syl5eq 2805 . . . . . . . . 9 (𝜑 → ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
10147, 78mulneg1d 11144 . . . . . . . . . 10 (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
10248, 31, 34, 56, 54, 31itgmulc2nclem2 35438 . . . . . . . . . 10 (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
103101, 102eqtr3d 2795 . . . . . . . . 9 (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
10495, 100, 1033eqtrd 2797 . . . . . . . 8 (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
10594, 104oveq12d 7174 . . . . . . 7 (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
10669, 58addcomd 10893 . . . . . . 7 (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
107105, 106eqtrd 2793 . . . . . 6 (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
10889, 90, 1073eqtrd 2797 . . . . 5 (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
10988, 108oveq12d 7174 . . . 4 (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
11074, 109eqtrd 2793 . . 3 (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
11159, 32mulcld 10712 . . . . . 6 ((𝜑𝑥𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
11218, 59, 31, 62, 35offval2 7430 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) = (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))))
11338, 46, 39mbfmulc2re 24361 . . . . . . . 8 (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
114112, 113eqeltrrd 2853 . . . . . . 7 (𝜑 → (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
11547, 31, 34, 114iblmulc2nc 35436 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
1161adantr 484 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
117116, 9mulcld 10712 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐶 · 𝐵) ∈ ℂ)
118 eqidd 2759 . . . . . . . . 9 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) = (𝑥𝐴 ↦ (𝐶 · 𝐵)))
119 ref 14532 . . . . . . . . . . 11 ℜ:ℂ⟶ℝ
120119a1i 11 . . . . . . . . . 10 (𝜑 → ℜ:ℂ⟶ℝ)
121120feqmptd 6726 . . . . . . . . 9 (𝜑 → ℜ = (𝑘 ∈ ℂ ↦ (ℜ‘𝑘)))
122 fveq2 6663 . . . . . . . . 9 (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵)))
123117, 118, 121, 122fmptco 6888 . . . . . . . 8 (𝜑 → (ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) = (𝑥𝐴 ↦ (ℜ‘(𝐶 · 𝐵))))
124116, 9remuld 14638 . . . . . . . . 9 ((𝜑𝑥𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))
125124mpteq2dva 5131 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
126123, 125eqtrd 2793 . . . . . . 7 (𝜑 → (ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) = (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
127117fmpttd 6876 . . . . . . . . . 10 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
128 ismbfcn 24342 . . . . . . . . . 10 ((𝑥𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
129127, 128syl 17 . . . . . . . . 9 (𝜑 → ((𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
13016, 129mpbid 235 . . . . . . . 8 (𝜑 → ((ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))
131130simpld 498 . . . . . . 7 (𝜑 → (ℜ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
132126, 131eqeltrrd 2853 . . . . . 6 (𝜑 → (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn)
13312, 28, 111, 115, 132itgsubnc 35433 . . . . 5 (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
134124itgeq2dv 24494 . . . . 5 (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥)
135111, 115itgneg 24516 . . . . . . . 8 (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
13659, 32mulneg1d 11144 . . . . . . . . 9 ((𝜑𝑥𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵)))
137136itgeq2dv 24494 . . . . . . . 8 (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
138135, 137eqtr4d 2796 . . . . . . 7 (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
139138oveq2d 7172 . . . . . 6 (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
140111, 115itgcl 24496 . . . . . . 7 (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
14129, 140negsubd 11054 . . . . . 6 (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
142139, 141eqtr3d 2795 . . . . 5 (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
143133, 134, 1423eqtr4d 2803 . . . 4 (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
144116, 9immuld 14639 . . . . . . . 8 ((𝜑𝑥𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))
145144itgeq2dv 24494 . . . . . . 7 (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥)
146 imf 14533 . . . . . . . . . . . . 13 ℑ:ℂ⟶ℝ
147146a1i 11 . . . . . . . . . . . 12 (𝜑 → ℑ:ℂ⟶ℝ)
148147feqmptd 6726 . . . . . . . . . . 11 (𝜑 → ℑ = (𝑘 ∈ ℂ ↦ (ℑ‘𝑘)))
149 fveq2 6663 . . . . . . . . . . 11 (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵)))
150117, 118, 148, 149fmptco 6888 . . . . . . . . . 10 (𝜑 → (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) = (𝑥𝐴 ↦ (ℑ‘(𝐶 · 𝐵))))
151144mpteq2dva 5131 . . . . . . . . . 10 (𝜑 → (𝑥𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
152150, 151eqtrd 2793 . . . . . . . . 9 (𝜑 → (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) = (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
153130simprd 499 . . . . . . . . 9 (𝜑 → (ℑ ∘ (𝑥𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
154152, 153eqeltrrd 2853 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn)
15533, 42, 60, 66, 154itgaddnc 35431 . . . . . . 7 (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
156145, 155eqtrd 2793 . . . . . 6 (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
157156oveq2d 7172 . . . . 5 (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
15871, 43, 67adddid 10716 . . . . 5 (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
159157, 158eqtrd 2793 . . . 4 (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
160143, 159oveq12d 7174 . . 3 (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
16170, 110, 1603eqtr4d 2803 . 2 (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
1621replimd 14617 . . 3 (𝜑𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶))))
163162oveq1d 7171 . 2 (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥))
1641, 8, 5, 16iblmulc2nc 35436 . . 3 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
165117, 164itgcnval 24512 . 2 (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
166161, 163, 1653eqtr4d 2803 1 (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409  {csn 4525   ↦ cmpt 5116   × cxp 5526  dom cdm 5528   ∘ ccom 5532  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156   ∘f cof 7409  ℂcc 10586  ℝcr 10587  1c1 10589  ici 10590   + caddc 10591   · cmul 10593   − cmin 10921  -cneg 10922  ℜcre 14517  ℑcim 14518  volcvol 24176  MblFncmbf 24327  𝐿1cibl 24330  ∫citg 24331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-inf2 9150  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665  ax-pre-sup 10666  ax-addf 10667 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-disj 5002  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7411  df-ofr 7412  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-2o 8119  df-er 8305  df-map 8424  df-pm 8425  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-fi 8921  df-sup 8952  df-inf 8953  df-oi 9020  df-dju 9376  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-4 11752  df-n0 11948  df-z 12034  df-uz 12296  df-q 12402  df-rp 12444  df-xneg 12561  df-xadd 12562  df-xmul 12563  df-ioo 12796  df-ico 12798  df-icc 12799  df-fz 12953  df-fzo 13096  df-fl 13224  df-mod 13300  df-seq 13432  df-exp 13493  df-hash 13754  df-cj 14519  df-re 14520  df-im 14521  df-sqrt 14655  df-abs 14656  df-clim 14906  df-sum 15104  df-rest 16767  df-topgen 16788  df-psmet 20171  df-xmet 20172  df-met 20173  df-bl 20174  df-mopn 20175  df-top 21607  df-topon 21624  df-bases 21659  df-cmp 22100  df-ovol 24177  df-vol 24178  df-mbf 24332  df-itg1 24333  df-itg2 24334  df-ibl 24335  df-itg 24336  df-0p 24383 This theorem is referenced by:  itgabsnc  35440
 Copyright terms: Public domain W3C validator