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 37217
Description: Choice-free analogue of itgmulc2 25779. (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 15171 . . . . . . . 8 (πœ‘ β†’ (β„œβ€˜πΆ) ∈ ℝ)
32recnd 11270 . . . . . . 7 (πœ‘ β†’ (β„œβ€˜πΆ) ∈ β„‚)
43adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜πΆ) ∈ β„‚)
5 itgmulc2nc.3 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1)
6 iblmbf 25713 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ MblFn)
75, 6syl 17 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ MblFn)
8 itgmulc2nc.2 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐡 ∈ 𝑉)
97, 8mbfmptcl 25581 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐡 ∈ β„‚)
109recld 15171 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜π΅) ∈ ℝ)
1110recnd 11270 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜π΅) ∈ β„‚)
124, 11mulcld 11262 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) ∈ β„‚)
139iblcn 25744 . . . . . . . 8 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ 𝐡) ∈ 𝐿1 ↔ ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 ∧ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1)))
145, 13mpbid 231 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 ∧ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1))
1514simpld 493 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1)
16 itgmulc2nc.m . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn)
17 ovexd 7450 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝐢 Β· 𝐡) ∈ V)
1816, 17mbfdm2 25582 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ dom vol)
19 fconstmpt 5734 . . . . . . . . 9 (𝐴 Γ— {(β„œβ€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜πΆ))
2019a1i 11 . . . . . . . 8 (πœ‘ β†’ (𝐴 Γ— {(β„œβ€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜πΆ)))
21 eqidd 2726 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)))
2218, 4, 10, 20, 21offval2 7701 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))))
23 iblmbf 25713 . . . . . . . . 9 ((π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ MblFn)
2415, 23syl 17 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)) ∈ MblFn)
2511fmpttd 7119 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅)):π΄βŸΆβ„‚)
2624, 2, 25mbfmulc2re 25593 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) ∈ MblFn)
2722, 26eqeltrrd 2826 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))) ∈ MblFn)
283, 10, 15, 27iblmulc2nc 37214 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„œβ€˜π΅))) ∈ 𝐿1)
2912, 28itgcl 25729 . . . 4 (πœ‘ β†’ ∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚)
30 ax-icn 11195 . . . . 5 i ∈ β„‚
319imcld 15172 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜π΅) ∈ ℝ)
3231recnd 11270 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜π΅) ∈ β„‚)
334, 32mulcld 11262 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
3414simprd 494 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1)
35 eqidd 2726 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)))
3618, 4, 31, 20, 35offval2 7701 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))))
37 iblmbf 25713 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ 𝐿1 β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ MblFn)
3834, 37syl 17 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)) ∈ MblFn)
3932fmpttd 7119 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅)):π΄βŸΆβ„‚)
4038, 2, 39mbfmulc2re 25593 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„œβ€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
4136, 40eqeltrrd 2826 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
423, 31, 34, 41iblmulc2nc 37214 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„œβ€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
4333, 42itgcl 25729 . . . . 5 (πœ‘ β†’ ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
44 mulcl 11220 . . . . 5 ((i ∈ β„‚ ∧ ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) ∈ β„‚)
4530, 43, 44sylancr 585 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) ∈ β„‚)
461imcld 15172 . . . . . . . . 9 (πœ‘ β†’ (β„‘β€˜πΆ) ∈ ℝ)
4746recnd 11270 . . . . . . . 8 (πœ‘ β†’ (β„‘β€˜πΆ) ∈ β„‚)
4847negcld 11586 . . . . . . 7 (πœ‘ β†’ -(β„‘β€˜πΆ) ∈ β„‚)
4948adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ -(β„‘β€˜πΆ) ∈ β„‚)
5049, 32mulcld 11262 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
51 fconstmpt 5734 . . . . . . . . 9 (𝐴 Γ— {-(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ -(β„‘β€˜πΆ))
5251a1i 11 . . . . . . . 8 (πœ‘ β†’ (𝐴 Γ— {-(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ -(β„‘β€˜πΆ)))
5318, 49, 31, 52, 35offval2 7701 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {-(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
5446renegcld 11669 . . . . . . . 8 (πœ‘ β†’ -(β„‘β€˜πΆ) ∈ ℝ)
5538, 54, 39mbfmulc2re 25593 . . . . . . 7 (πœ‘ β†’ ((𝐴 Γ— {-(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
5653, 55eqeltrrd 2826 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
5748, 31, 34, 56iblmulc2nc 37214 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
5850, 57itgcl 25729 . . . 4 (πœ‘ β†’ ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
5947adantr 479 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜πΆ) ∈ β„‚)
6059, 11mulcld 11262 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) ∈ β„‚)
61 fconstmpt 5734 . . . . . . . . . 10 (𝐴 Γ— {(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜πΆ))
6261a1i 11 . . . . . . . . 9 (πœ‘ β†’ (𝐴 Γ— {(β„‘β€˜πΆ)}) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜πΆ)))
6318, 59, 10, 62, 21offval2 7701 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))))
6424, 46, 25mbfmulc2re 25593 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜π΅))) ∈ MblFn)
6563, 64eqeltrrd 2826 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) ∈ MblFn)
6647, 10, 15, 65iblmulc2nc 37214 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) ∈ 𝐿1)
6760, 66itgcl 25729 . . . . 5 (πœ‘ β†’ ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚)
68 mulcl 11220 . . . . 5 ((i ∈ β„‚ ∧ ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) ∈ β„‚)
6930, 67, 68sylancr 585 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) ∈ β„‚)
7029, 45, 58, 69add4d 11470 . . 3 (πœ‘ β†’ ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
7130a1i 11 . . . . . 6 (πœ‘ β†’ i ∈ β„‚)
7271, 47mulcld 11262 . . . . 5 (πœ‘ β†’ (i Β· (β„‘β€˜πΆ)) ∈ β„‚)
738, 5itgcl 25729 . . . . 5 (πœ‘ β†’ ∫𝐴𝐡 dπ‘₯ ∈ β„‚)
743, 72, 73adddird 11267 . . . 4 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = (((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯)))
758, 5itgcnval 25745 . . . . . . 7 (πœ‘ β†’ ∫𝐴𝐡 dπ‘₯ = (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
7675oveq2d 7431 . . . . . 6 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) = ((β„œβ€˜πΆ) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
7710, 15itgcl 25729 . . . . . . 7 (πœ‘ β†’ ∫𝐴(β„œβ€˜π΅) dπ‘₯ ∈ β„‚)
7831, 34itgcl 25729 . . . . . . . 8 (πœ‘ β†’ ∫𝐴(β„‘β€˜π΅) dπ‘₯ ∈ β„‚)
79 mulcl 11220 . . . . . . . 8 ((i ∈ β„‚ ∧ ∫𝐴(β„‘β€˜π΅) dπ‘₯ ∈ β„‚) β†’ (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
8030, 78, 79sylancr 585 . . . . . . 7 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
813, 77, 80adddid 11266 . . . . . 6 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
823, 10, 15, 27, 2, 10itgmulc2nclem2 37216 . . . . . . 7 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = ∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)
833, 71, 78mul12d 11451 . . . . . . . 8 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
843, 31, 34, 41, 2, 31itgmulc2nclem2 37216 . . . . . . . . 9 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
8584oveq2d 7431 . . . . . . . 8 (πœ‘ β†’ (i Β· ((β„œβ€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
8683, 85eqtrd 2765 . . . . . . 7 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
8782, 86oveq12d 7433 . . . . . 6 (πœ‘ β†’ (((β„œβ€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((β„œβ€˜πΆ) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)))
8876, 81, 873eqtrd 2769 . . . . 5 (πœ‘ β†’ ((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)))
8975oveq2d 7431 . . . . . 6 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯) = ((i Β· (β„‘β€˜πΆ)) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
9072, 77, 80adddid 11266 . . . . . 6 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (∫𝐴(β„œβ€˜π΅) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))))
9171, 47, 77mulassd 11265 . . . . . . . . 9 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = (i Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯)))
9247, 10, 15, 65, 46, 10itgmulc2nclem2 37216 . . . . . . . . . 10 (πœ‘ β†’ ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)
9392oveq2d 7431 . . . . . . . . 9 (πœ‘ β†’ (i Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯)) = (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
9491, 93eqtrd 2765 . . . . . . . 8 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) = (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
9571, 47, 71, 78mul4d 11454 . . . . . . . . 9 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)))
96 ixi 11871 . . . . . . . . . . 11 (i Β· i) = -1
9796oveq1i 7425 . . . . . . . . . 10 ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = (-1 Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
9847, 78mulcld 11262 . . . . . . . . . . 11 (πœ‘ β†’ ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) ∈ β„‚)
9998mulm1d 11694 . . . . . . . . . 10 (πœ‘ β†’ (-1 Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10097, 99eqtrid 2777 . . . . . . . . 9 (πœ‘ β†’ ((i Β· i) Β· ((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10147, 78mulneg1d 11695 . . . . . . . . . 10 (πœ‘ β†’ (-(β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))
10248, 31, 34, 56, 54, 31itgmulc2nclem2 37216 . . . . . . . . . 10 (πœ‘ β†’ (-(β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
103101, 102eqtr3d 2767 . . . . . . . . 9 (πœ‘ β†’ -((β„‘β€˜πΆ) Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
10495, 100, 1033eqtrd 2769 . . . . . . . 8 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯)) = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
10594, 104oveq12d 7433 . . . . . . 7 (πœ‘ β†’ (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = ((i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
10669, 58addcomd 11444 . . . . . . 7 (πœ‘ β†’ ((i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯) + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
107105, 106eqtrd 2765 . . . . . 6 (πœ‘ β†’ (((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴(β„œβ€˜π΅) dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· (i Β· ∫𝐴(β„‘β€˜π΅) dπ‘₯))) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
10889, 90, 1073eqtrd 2769 . . . . 5 (πœ‘ β†’ ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
10988, 108oveq12d 7433 . . . 4 (πœ‘ β†’ (((β„œβ€˜πΆ) Β· ∫𝐴𝐡 dπ‘₯) + ((i Β· (β„‘β€˜πΆ)) Β· ∫𝐴𝐡 dπ‘₯)) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
11074, 109eqtrd 2765 . . 3 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)) + (∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
11159, 32mulcld 11262 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) ∈ β„‚)
11218, 59, 31, 62, 35offval2 7701 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) = (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
11338, 46, 39mbfmulc2re 25593 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {(β„‘β€˜πΆ)}) ∘f Β· (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜π΅))) ∈ MblFn)
114112, 113eqeltrrd 2826 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ MblFn)
11547, 31, 34, 114iblmulc2nc 37214 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) ∈ 𝐿1)
1161adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝐢 ∈ β„‚)
117116, 9mulcld 11262 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝐢 Β· 𝐡) ∈ β„‚)
118 eqidd 2726 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) = (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)))
119 ref 15089 . . . . . . . . . . 11 β„œ:β„‚βŸΆβ„
120119a1i 11 . . . . . . . . . 10 (πœ‘ β†’ β„œ:β„‚βŸΆβ„)
121120feqmptd 6961 . . . . . . . . 9 (πœ‘ β†’ β„œ = (π‘˜ ∈ β„‚ ↦ (β„œβ€˜π‘˜)))
122 fveq2 6891 . . . . . . . . 9 (π‘˜ = (𝐢 Β· 𝐡) β†’ (β„œβ€˜π‘˜) = (β„œβ€˜(𝐢 Β· 𝐡)))
123117, 118, 121, 122fmptco 7133 . . . . . . . 8 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜(𝐢 Β· 𝐡))))
124116, 9remuld 15195 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„œβ€˜(𝐢 Β· 𝐡)) = (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))))
125124mpteq2dva 5243 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„œβ€˜(𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))))
126123, 125eqtrd 2765 . . . . . . 7 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))))
127117fmpttd 7119 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)):π΄βŸΆβ„‚)
128 ismbfcn 25574 . . . . . . . . . 10 ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)):π΄βŸΆβ„‚ β†’ ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn ↔ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)))
129127, 128syl 17 . . . . . . . . 9 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ MblFn ↔ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)))
13016, 129mpbid 231 . . . . . . . 8 (πœ‘ β†’ ((β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn ∧ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn))
131130simpld 493 . . . . . . 7 (πœ‘ β†’ (β„œ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)
132126, 131eqeltrrd 2826 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))) ∈ MblFn)
13312, 28, 111, 115, 132itgsubnc 37211 . . . . 5 (πœ‘ β†’ ∫𝐴(((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
134124itgeq2dv 25727 . . . . 5 (πœ‘ β†’ ∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ = ∫𝐴(((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) βˆ’ ((β„‘β€˜πΆ) Β· (β„‘β€˜π΅))) dπ‘₯)
135111, 115itgneg 25749 . . . . . . . 8 (πœ‘ β†’ -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴-((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
13659, 32mulneg1d 11695 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) = -((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)))
137136itgeq2dv 25727 . . . . . . . 8 (πœ‘ β†’ ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴-((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
138135, 137eqtr4d 2768 . . . . . . 7 (πœ‘ β†’ -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ = ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯)
139138oveq2d 7431 . . . . . 6 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
140111, 115itgcl 25729 . . . . . . 7 (πœ‘ β†’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ ∈ β„‚)
14129, 140negsubd 11605 . . . . . 6 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + -∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
142139, 141eqtr3d 2767 . . . . 5 (πœ‘ β†’ (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ βˆ’ ∫𝐴((β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
143133, 134, 1423eqtr4d 2775 . . . 4 (πœ‘ β†’ ∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯))
144116, 9immuld 15196 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (β„‘β€˜(𝐢 Β· 𝐡)) = (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))))
145144itgeq2dv 25727 . . . . . . 7 (πœ‘ β†’ ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯ = ∫𝐴(((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) dπ‘₯)
146 imf 15090 . . . . . . . . . . . . 13 β„‘:β„‚βŸΆβ„
147146a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ β„‘:β„‚βŸΆβ„)
148147feqmptd 6961 . . . . . . . . . . 11 (πœ‘ β†’ β„‘ = (π‘˜ ∈ β„‚ ↦ (β„‘β€˜π‘˜)))
149 fveq2 6891 . . . . . . . . . . 11 (π‘˜ = (𝐢 Β· 𝐡) β†’ (β„‘β€˜π‘˜) = (β„‘β€˜(𝐢 Β· 𝐡)))
150117, 118, 148, 149fmptco 7133 . . . . . . . . . 10 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜(𝐢 Β· 𝐡))))
151144mpteq2dva 5243 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (β„‘β€˜(𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))))
152150, 151eqtrd 2765 . . . . . . . . 9 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) = (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))))
153130simprd 494 . . . . . . . . 9 (πœ‘ β†’ (β„‘ ∘ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡))) ∈ MblFn)
154152, 153eqeltrrd 2826 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)))) ∈ MblFn)
15533, 42, 60, 66, 154itgaddnc 37209 . . . . . . 7 (πœ‘ β†’ ∫𝐴(((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) + ((β„‘β€˜πΆ) Β· (β„œβ€˜π΅))) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
156145, 155eqtrd 2765 . . . . . 6 (πœ‘ β†’ ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯ = (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))
157156oveq2d 7431 . . . . 5 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯) = (i Β· (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
15871, 43, 67adddid 11266 . . . . 5 (πœ‘ β†’ (i Β· (∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯ + ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)) = ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
159157, 158eqtrd 2765 . . . 4 (πœ‘ β†’ (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯) = ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯)))
160143, 159oveq12d 7433 . . 3 (πœ‘ β†’ (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)) = ((∫𝐴((β„œβ€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯ + ∫𝐴(-(β„‘β€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + ((i Β· ∫𝐴((β„œβ€˜πΆ) Β· (β„‘β€˜π΅)) dπ‘₯) + (i Β· ∫𝐴((β„‘β€˜πΆ) Β· (β„œβ€˜π΅)) dπ‘₯))))
16170, 110, 1603eqtr4d 2775 . 2 (πœ‘ β†’ (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯) = (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)))
1621replimd 15174 . . 3 (πœ‘ β†’ 𝐢 = ((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))))
163162oveq1d 7430 . 2 (πœ‘ β†’ (𝐢 Β· ∫𝐴𝐡 dπ‘₯) = (((β„œβ€˜πΆ) + (i Β· (β„‘β€˜πΆ))) Β· ∫𝐴𝐡 dπ‘₯))
1641, 8, 5, 16iblmulc2nc 37214 . . 3 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ (𝐢 Β· 𝐡)) ∈ 𝐿1)
165117, 164itgcnval 25745 . 2 (πœ‘ β†’ ∫𝐴(𝐢 Β· 𝐡) dπ‘₯ = (∫𝐴(β„œβ€˜(𝐢 Β· 𝐡)) dπ‘₯ + (i Β· ∫𝐴(β„‘β€˜(𝐢 Β· 𝐡)) dπ‘₯)))
166161, 163, 1653eqtr4d 2775 1 (πœ‘ β†’ (𝐢 Β· ∫𝐴𝐡 dπ‘₯) = ∫𝐴(𝐢 Β· 𝐡) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Vcvv 3463  {csn 4624   ↦ cmpt 5226   Γ— cxp 5670  dom cdm 5672   ∘ ccom 5676  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7415   ∘f cof 7679  β„‚cc 11134  β„cr 11135  1c1 11137  ici 11138   + caddc 11139   Β· cmul 11141   βˆ’ cmin 11472  -cneg 11473  β„œcre 15074  β„‘cim 15075  volcvol 25408  MblFncmbf 25559  πΏ1cibl 25562  βˆ«citg 25563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-inf2 9662  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214  ax-addf 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-disj 5109  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7681  df-ofr 7682  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-2o 8484  df-er 8721  df-map 8843  df-pm 8844  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-fi 9432  df-sup 9463  df-inf 9464  df-oi 9531  df-dju 9922  df-card 9960  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-n0 12501  df-z 12587  df-uz 12851  df-q 12961  df-rp 13005  df-xneg 13122  df-xadd 13123  df-xmul 13124  df-ioo 13358  df-ico 13360  df-icc 13361  df-fz 13515  df-fzo 13658  df-fl 13787  df-mod 13865  df-seq 13997  df-exp 14057  df-hash 14320  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-clim 15462  df-sum 15663  df-rest 17401  df-topgen 17422  df-psmet 21273  df-xmet 21274  df-met 21275  df-bl 21276  df-mopn 21277  df-top 22812  df-topon 22829  df-bases 22865  df-cmp 23307  df-ovol 25409  df-vol 25410  df-mbf 25564  df-itg1 25565  df-itg2 25566  df-ibl 25567  df-itg 25568  df-0p 25615
This theorem is referenced by:  itgabsnc  37218
  Copyright terms: Public domain W3C validator