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

Theorem itgmulc2nc 36149
Description: Choice-free analogue of itgmulc2 25201. (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 15080 . . . . . . . 8 (πœ‘ β†’ (β„œβ€˜πΆ) ∈ ℝ)
32recnd 11184 . . . . . . 7 (πœ‘ β†’ (β„œβ€˜πΆ) ∈ β„‚)
43adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜πΆ) ∈ β„‚)
5 itgmulc2nc.3 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1)
6 iblmbf 25135 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ MblFn)
75, 6syl 17 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ MblFn)
8 itgmulc2nc.2 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐡 ∈ 𝑉)
97, 8mbfmptcl 25003 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
109recld 15080 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜π΅) ∈ ℝ)
1110recnd 11184 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜π΅) ∈ β„‚)
124, 11mulcld 11176 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) ∈ β„‚)
139iblcn 25166 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1 ↔ ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 ∧ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1)))
145, 13mpbid 231 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 ∧ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1))
1514simpld 496 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1)
16 itgmulc2nc.m . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn)
17 ovexd 7393 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝐢 Β· 𝐡) ∈ V)
1816, 17mbfdm2 25004 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ dom vol)
19 fconstmpt 5695 . . . . . . . . 9 (𝐴 Γ— {(β„œβ€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜πΆ))
2019a1i 11 . . . . . . . 8 (πœ‘ β†’ (𝐴 Γ— {(β„œβ€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜πΆ)))
21 eqidd 2738 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)))
2218, 4, 10, 20, 21offval2 7638 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))))
23 iblmbf 25135 . . . . . . . . 9 ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ MblFn)
2415, 23syl 17 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ MblFn)
2511fmpttd 7064 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)):π΄βŸΆβ„‚)
2624, 2, 25mbfmulc2re 25015 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) ∈ MblFn)
2722, 26eqeltrrd 2839 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))) ∈ MblFn)
283, 10, 15, 27iblmulc2nc 36146 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))) ∈ 𝐿1)
2912, 28itgcl 25151 . . . 4 (πœ‘ β†’ ∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚)
30 ax-icn 11111 . . . . 5 i ∈ β„‚
319imcld 15081 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜π΅) ∈ ℝ)
3231recnd 11184 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜π΅) ∈ β„‚)
334, 32mulcld 11176 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
3414simprd 497 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1)
35 eqidd 2738 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)))
3618, 4, 31, 20, 35offval2 7638 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))))
37 iblmbf 25135 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ MblFn)
3834, 37syl 17 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ MblFn)
3932fmpttd 7064 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)):π΄βŸΆβ„‚)
4038, 2, 39mbfmulc2re 25015 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
4136, 40eqeltrrd 2839 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
423, 31, 34, 41iblmulc2nc 36146 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
4333, 42itgcl 25151 . . . . 5 (πœ‘ β†’ ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
44 mulcl 11136 . . . . 5 ((i ∈ β„‚ ∧ ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) ∈ β„‚)
4530, 43, 44sylancr 588 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) ∈ β„‚)
461imcld 15081 . . . . . . . . 9 (πœ‘ β†’ (β„‘β€˜πΆ) ∈ ℝ)
4746recnd 11184 . . . . . . . 8 (πœ‘ β†’ (β„‘β€˜πΆ) ∈ β„‚)
4847negcld 11500 . . . . . . 7 (πœ‘ β†’ -(β„‘β€˜πΆ) ∈ β„‚)
4948adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ -(β„‘β€˜πΆ) ∈ β„‚)
5049, 32mulcld 11176 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
51 fconstmpt 5695 . . . . . . . . 9 (𝐴 Γ— {-(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ -(β„‘β€˜πΆ))
5251a1i 11 . . . . . . . 8 (πœ‘ β†’ (𝐴 Γ— {-(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ -(β„‘β€˜πΆ)))
5318, 49, 31, 52, 35offval2 7638 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {-(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
5446renegcld 11583 . . . . . . . 8 (πœ‘ β†’ -(β„‘β€˜πΆ) ∈ ℝ)
5538, 54, 39mbfmulc2re 25015 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {-(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
5653, 55eqeltrrd 2839 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
5748, 31, 34, 56iblmulc2nc 36146 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
5850, 57itgcl 25151 . . . 4 (πœ‘ β†’ ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
5947adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜πΆ) ∈ β„‚)
6059, 11mulcld 11176 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) ∈ β„‚)
61 fconstmpt 5695 . . . . . . . . . 10 (𝐴 Γ— {(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜πΆ))
6261a1i 11 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Γ— {(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜πΆ)))
6318, 59, 10, 62, 21offval2 7638 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))))
6424, 46, 25mbfmulc2re 25015 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) ∈ MblFn)
6563, 64eqeltrrd 2839 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) ∈ MblFn)
6647, 10, 15, 65iblmulc2nc 36146 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) ∈ 𝐿1)
6760, 66itgcl 25151 . . . . 5 (πœ‘ β†’ ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚)
68 mulcl 11136 . . . . 5 ((i ∈ β„‚ ∧ ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) ∈ β„‚)
6930, 67, 68sylancr 588 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) ∈ β„‚)
7029, 45, 58, 69add4d 11384 . . 3 (πœ‘ β†’ ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
7130a1i 11 . . . . . 6 (πœ‘ β†’ i ∈ β„‚)
7271, 47mulcld 11176 . . . . 5 (πœ‘ β†’ (i Β· (β„‘β€˜πΆ)) ∈ β„‚)
738, 5itgcl 25151 . . . . 5 (πœ‘ β†’ ∫𝐴𝐡 dπ‘₯ ∈ β„‚)
743, 72, 73adddird 11181 . . . 4 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = (((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯)))
758, 5itgcnval 25167 . . . . . . 7 (πœ‘ β†’ ∫𝐴𝐡 dπ‘₯ = (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
7675oveq2d 7374 . . . . . 6 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) = ((β„œβ€˜πΆ) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
7710, 15itgcl 25151 . . . . . . 7 (πœ‘ β†’ ∫𝐴(β„œβ€˜π΅) dπ‘₯ ∈ β„‚)
7831, 34itgcl 25151 . . . . . . . 8 (πœ‘ β†’ ∫𝐴(β„‘β€˜π΅) dπ‘₯ ∈ β„‚)
79 mulcl 11136 . . . . . . . 8 ((i ∈ β„‚ ∧ ∫𝐴(β„‘β€˜π΅) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
8030, 78, 79sylancr 588 . . . . . . 7 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
813, 77, 80adddid 11180 . . . . . 6 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
823, 10, 15, 27, 2, 10itgmulc2nclem2 36148 . . . . . . 7 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = ∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)
833, 71, 78mul12d 11365 . . . . . . . 8 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
843, 31, 34, 41, 2, 31itgmulc2nclem2 36148 . . . . . . . . 9 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
8584oveq2d 7374 . . . . . . . 8 (πœ‘ β†’ (i Β· ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
8683, 85eqtrd 2777 . . . . . . 7 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
8782, 86oveq12d 7376 . . . . . 6 (πœ‘ β†’ (((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)))
8876, 81, 873eqtrd 2781 . . . . 5 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)))
8975oveq2d 7374 . . . . . 6 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯) = ((i Β· (β„‘β€˜πΆ)) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
9072, 77, 80adddid 11180 . . . . . 6 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
9171, 47, 77mulassd 11179 . . . . . . . . 9 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = (i Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯)))
9247, 10, 15, 65, 46, 10itgmulc2nclem2 36148 . . . . . . . . . 10 (πœ‘ β†’ ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)
9392oveq2d 7374 . . . . . . . . 9 (πœ‘ β†’ (i Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
9491, 93eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
9571, 47, 71, 78mul4d 11368 . . . . . . . . 9 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
96 ixi 11785 . . . . . . . . . . 11 (i Β· i) = -1
9796oveq1i 7368 . . . . . . . . . 10 ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (-1 Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
9847, 78mulcld 11176 . . . . . . . . . . 11 (πœ‘ β†’ ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
9998mulm1d 11608 . . . . . . . . . 10 (πœ‘ β†’ (-1 Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10097, 99eqtrid 2789 . . . . . . . . 9 (πœ‘ β†’ ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10147, 78mulneg1d 11609 . . . . . . . . . 10 (πœ‘ β†’ (-(β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10248, 31, 34, 56, 54, 31itgmulc2nclem2 36148 . . . . . . . . . 10 (πœ‘ β†’ (-(β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
103101, 102eqtr3d 2779 . . . . . . . . 9 (πœ‘ β†’ -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
10495, 100, 1033eqtrd 2781 . . . . . . . 8 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
10594, 104oveq12d 7376 . . . . . . 7 (πœ‘ β†’ (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = ((i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
10669, 58addcomd 11358 . . . . . . 7 (πœ‘ β†’ ((i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
107105, 106eqtrd 2777 . . . . . 6 (πœ‘ β†’ (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
10889, 90, 1073eqtrd 2781 . . . . 5 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
10988, 108oveq12d 7376 . . . 4 (πœ‘ β†’ (((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯)) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
11074, 109eqtrd 2777 . . 3 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
11159, 32mulcld 11176 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
11218, 59, 31, 62, 35offval2 7638 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
11338, 46, 39mbfmulc2re 25015 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
114112, 113eqeltrrd 2839 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
11547, 31, 34, 114iblmulc2nc 36146 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
1161adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐢 ∈ β„‚)
117116, 9mulcld 11176 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝐢 Β· 𝐡) ∈ β„‚)
118 eqidd 2738 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) = (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)))
119 ref 14998 . . . . . . . . . . 11 β„œ:β„‚βŸΆβ„
120119a1i 11 . . . . . . . . . 10 (πœ‘ β†’ β„œ:β„‚βŸΆβ„)
121120feqmptd 6911 . . . . . . . . 9 (πœ‘ β†’ β„œ = (π‘˜ ∈ β„‚ ↦ (β„œβ€˜π‘˜)))
122 fveq2 6843 . . . . . . . . 9 (π‘˜ = (𝐢 Β· 𝐡) β†’ (β„œβ€˜π‘˜) = (β„œβ€˜(𝐢 Β· 𝐡)))
123117, 118, 121, 122fmptco 7076 . . . . . . . 8 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜(𝐢 Β· 𝐡))))
124116, 9remuld 15104 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜(𝐢 Β· 𝐡)) = (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
125124mpteq2dva 5206 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜(𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))))
126123, 125eqtrd 2777 . . . . . . 7 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))))
127117fmpttd 7064 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)):π΄βŸΆβ„‚)
128 ismbfcn 24996 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)):π΄βŸΆβ„‚ β†’ ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn ↔ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)))
129127, 128syl 17 . . . . . . . . 9 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn ↔ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)))
13016, 129mpbid 231 . . . . . . . 8 (πœ‘ β†’ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn))
131130simpld 496 . . . . . . 7 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)
132126, 131eqeltrrd 2839 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))) ∈ MblFn)
13312, 28, 111, 115, 132itgsubnc 36143 . . . . 5 (πœ‘ β†’ ∫𝐴(((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
134124itgeq2dv 25149 . . . . 5 (πœ‘ β†’ ∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ = ∫𝐴(((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) dπ‘₯)
135111, 115itgneg 25171 . . . . . . . 8 (πœ‘ β†’ -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴-((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
13659, 32mulneg1d 11609 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) = -((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))
137136itgeq2dv 25149 . . . . . . . 8 (πœ‘ β†’ ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴-((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
138135, 137eqtr4d 2780 . . . . . . 7 (πœ‘ β†’ -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
139138oveq2d 7374 . . . . . 6 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
140111, 115itgcl 25151 . . . . . . 7 (πœ‘ β†’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
14129, 140negsubd 11519 . . . . . 6 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
142139, 141eqtr3d 2779 . . . . 5 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
143133, 134, 1423eqtr4d 2787 . . . 4 (πœ‘ β†’ ∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
144116, 9immuld 15105 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜(𝐢 Β· 𝐡)) = (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))))
145144itgeq2dv 25149 . . . . . . 7 (πœ‘ β†’ ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯ = ∫𝐴(((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) dπ‘₯)
146 imf 14999 . . . . . . . . . . . . 13 β„‘:β„‚βŸΆβ„
147146a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ β„‘:β„‚βŸΆβ„)
148147feqmptd 6911 . . . . . . . . . . 11 (πœ‘ β†’ β„‘ = (π‘˜ ∈ β„‚ ↦ (β„‘β€˜π‘˜)))
149 fveq2 6843 . . . . . . . . . . 11 (π‘˜ = (𝐢 Β· 𝐡) β†’ (β„‘β€˜π‘˜) = (β„‘β€˜(𝐢 Β· 𝐡)))
150117, 118, 148, 149fmptco 7076 . . . . . . . . . 10 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜(𝐢 Β· 𝐡))))
151144mpteq2dva 5206 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜(𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))))
152150, 151eqtrd 2777 . . . . . . . . 9 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))))
153130simprd 497 . . . . . . . . 9 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)
154152, 153eqeltrrd 2839 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))) ∈ MblFn)
15533, 42, 60, 66, 154itgaddnc 36141 . . . . . . 7 (πœ‘ β†’ ∫𝐴(((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
156145, 155eqtrd 2777 . . . . . 6 (πœ‘ β†’ ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
157156oveq2d 7374 . . . . 5 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯) = (i Β· (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
15871, 43, 67adddid 11180 . . . . 5 (πœ‘ β†’ (i Β· (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)) = ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
159157, 158eqtrd 2777 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯) = ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
160143, 159oveq12d 7376 . . 3 (πœ‘ β†’ (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
16170, 110, 1603eqtr4d 2787 . 2 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)))
1621replimd 15083 . . 3 (πœ‘ β†’ 𝐢 = ((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))))
163162oveq1d 7373 . 2 (πœ‘ β†’ (𝐢 Β· ∫𝐴𝐡 dπ‘₯) = (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯))
1641, 8, 5, 16iblmulc2nc 36146 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ 𝐿1)
165117, 164itgcnval 25167 . 2 (πœ‘ β†’ ∫𝐴(𝐢 Β· 𝐡) dπ‘₯ = (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)))
166161, 163, 1653eqtr4d 2787 1 (πœ‘ β†’ (𝐢 Β· ∫𝐴𝐡 dπ‘₯) = ∫𝐴(𝐢 Β· 𝐡) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3446  {csn 4587   ↦ cmpt 5189   Γ— cxp 5632  dom cdm 5634   ∘ ccom 5638  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358   ∘f cof 7616  β„‚cc 11050  β„cr 11051  1c1 11053  ici 11054   + caddc 11055   Β· cmul 11057   βˆ’ cmin 11386  -cneg 11387  β„œcre 14983  β„‘cim 14984  volcvol 24830  MblFncmbf 24981  πΏ1cibl 24984  βˆ«citg 24985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9578  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130  ax-addf 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-ofr 7619  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8649  df-map 8768  df-pm 8769  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fi 9348  df-sup 9379  df-inf 9380  df-oi 9447  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-n0 12415  df-z 12501  df-uz 12765  df-q 12875  df-rp 12917  df-xneg 13034  df-xadd 13035  df-xmul 13036  df-ioo 13269  df-ico 13271  df-icc 13272  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-clim 15371  df-sum 15572  df-rest 17305  df-topgen 17326  df-psmet 20791  df-xmet 20792  df-met 20793  df-bl 20794  df-mopn 20795  df-top 22246  df-topon 22263  df-bases 22299  df-cmp 22741  df-ovol 24831  df-vol 24832  df-mbf 24986  df-itg1 24987  df-itg2 24988  df-ibl 24989  df-itg 24990  df-0p 25037
This theorem is referenced by:  itgabsnc  36150
  Copyright terms: Public domain W3C validator