Metamath Proof Explorer

Theorem itgmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 
|- ( ph -> C e. CC )
itgmulc2.2 
|- ( ( ph /\ x e. A ) -> B e. V )
itgmulc2.3 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgmulc2 
|- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgmulc2.1 
 |-  ( ph -> C e. CC )
2 itgmulc2.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 itgmulc2.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 1 recld 
 |-  ( ph -> ( Re ` C ) e. RR )
5 4 recnd 
 |-  ( ph -> ( Re ` C ) e. CC )
6 5 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC )
7 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
8 3 7 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
9 8 2 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
10 9 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
11 10 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
12 6 11 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Re ` B ) ) e. CC )
13 9 iblcn 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
14 3 13 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
15 14 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
16 5 10 15 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) e. L^1 )
17 12 16 itgcl 
 |-  ( ph -> S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x e. CC )
18 ax-icn 
 |-  _i e. CC
19 9 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
20 19 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
21 6 20 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Im ` B ) ) e. CC )
22 14 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
23 5 19 22 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) e. L^1 )
24 21 23 itgcl 
 |-  ( ph -> S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x e. CC )
25 mulcl 
 |-  ( ( _i e. CC /\ S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x e. CC ) -> ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) e. CC )
26 18 24 25 sylancr 
 |-  ( ph -> ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) e. CC )
27 1 imcld 
 |-  ( ph -> ( Im ` C ) e. RR )
28 27 renegcld 
 |-  ( ph -> -u ( Im ` C ) e. RR )
29 28 recnd 
 |-  ( ph -> -u ( Im ` C ) e. CC )
30 29 adantr 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. CC )
31 30 20 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) e. CC )
32 29 19 22 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) e. L^1 )
33 31 32 itgcl 
 |-  ( ph -> S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x e. CC )
34 27 recnd 
 |-  ( ph -> ( Im ` C ) e. CC )
35 34 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC )
36 35 11 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Re ` B ) ) e. CC )
37 34 10 15 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) e. L^1 )
38 36 37 itgcl 
 |-  ( ph -> S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x e. CC )
39 mulcl 
 |-  ( ( _i e. CC /\ S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x e. CC ) -> ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) e. CC )
40 18 38 39 sylancr 
 |-  ( ph -> ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) e. CC )
41 17 26 33 40 add4d 
 |-  ( ph -> ( ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) ) + ( S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) ) = ( ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) + ( ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) ) )
42 2 3 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
43 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` C ) e. CC ) -> ( _i x. ( Im ` C ) ) e. CC )
44 18 34 43 sylancr 
 |-  ( ph -> ( _i x. ( Im ` C ) ) e. CC )
45 2 3 itgcnval 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
46 45 oveq2d 
 |-  ( ph -> ( ( Re ` C ) x. S. A B _d x ) = ( ( Re ` C ) x. ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) )
47 10 15 itgcl 
 |-  ( ph -> S. A ( Re ` B ) _d x e. CC )
48 19 22 itgcl 
 |-  ( ph -> S. A ( Im ` B ) _d x e. CC )
49 mulcl 
 |-  ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
50 18 48 49 sylancr 
 |-  ( ph -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
51 5 47 50 adddid 
 |-  ( ph -> ( ( Re ` C ) x. ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) = ( ( ( Re ` C ) x. S. A ( Re ` B ) _d x ) + ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) ) )
52 5 10 15 4 10 itgmulc2lem2 
 |-  ( ph -> ( ( Re ` C ) x. S. A ( Re ` B ) _d x ) = S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x )
53 18 a1i 
 |-  ( ph -> _i e. CC )
54 5 53 48 mul12d 
 |-  ( ph -> ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = ( _i x. ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) ) )
55 5 19 22 4 19 itgmulc2lem2 
 |-  ( ph -> ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x )
56 55 oveq2d 
 |-  ( ph -> ( _i x. ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) ) = ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) )
57 54 56 eqtrd 
 |-  ( ph -> ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) )
58 52 57 oveq12d 
 |-  ( ph -> ( ( ( Re ` C ) x. S. A ( Re ` B ) _d x ) + ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) ) = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) ) )
59 46 51 58 3eqtrd 
 |-  ( ph -> ( ( Re ` C ) x. S. A B _d x ) = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) ) )
60 45 oveq2d 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A B _d x ) = ( ( _i x. ( Im ` C ) ) x. ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) )
61 44 47 50 adddid 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) = ( ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) + ( ( _i x. ( Im ` C ) ) x. ( _i x. S. A ( Im ` B ) _d x ) ) ) )
62 53 34 47 mulassd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) = ( _i x. ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) ) )
63 34 10 15 27 10 itgmulc2lem2 
 |-  ( ph -> ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) = S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x )
64 63 oveq2d 
 |-  ( ph -> ( _i x. ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) ) = ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
65 62 64 eqtrd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) = ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
66 53 34 53 48 mul4d 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = ( ( _i x. _i ) x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) ) )
67 ixi 
 |-  ( _i x. _i ) = -u 1
68 67 oveq1i 
 |-  ( ( _i x. _i ) x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) ) = ( -u 1 x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
69 34 48 mulcld 
 |-  ( ph -> ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) e. CC )
70 69 mulm1d 
 |-  ( ph -> ( -u 1 x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) ) = -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
71 68 70 eqtrid 
 |-  ( ph -> ( ( _i x. _i ) x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) ) = -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
72 34 48 mulneg1d 
 |-  ( ph -> ( -u ( Im ` C ) x. S. A ( Im ` B ) _d x ) = -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
73 29 19 22 28 19 itgmulc2lem2 
 |-  ( ph -> ( -u ( Im ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
74 72 73 eqtr3d 
 |-  ( ph -> -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
75 66 71 74 3eqtrd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
76 65 75 oveq12d 
 |-  ( ph -> ( ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) + ( ( _i x. ( Im ` C ) ) x. ( _i x. S. A ( Im ` B ) _d x ) ) ) = ( ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) )
77 40 33 76 comraddd 
 |-  ( ph -> ( ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) + ( ( _i x. ( Im ` C ) ) x. ( _i x. S. A ( Im ` B ) _d x ) ) ) = ( S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) )
78 60 61 77 3eqtrd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A B _d x ) = ( S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) )
79 59 78 oveq12d 
 |-  ( ph -> ( ( ( Re ` C ) x. S. A B _d x ) + ( ( _i x. ( Im ` C ) ) x. S. A B _d x ) ) = ( ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) ) + ( S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) ) )
80 5 42 44 79 joinlmuladdmuld 
 |-  ( ph -> ( ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) x. S. A B _d x ) = ( ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) ) + ( S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) ) )
81 35 20 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Im ` B ) ) e. CC )
82 12 81 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + -u ( ( Im ` C ) x. ( Im ` B ) ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) )
83 35 20 mulneg1d 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) = -u ( ( Im ` C ) x. ( Im ` B ) ) )
84 83 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) + -u ( ( Im ` C ) x. ( Im ` B ) ) ) )
85 1 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
86 85 9 remuld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) )
87 82 84 86 3eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) = ( Re ` ( C x. B ) ) )
88 87 itgeq2dv 
 |-  ( ph -> S. A ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) _d x = S. A ( Re ` ( C x. B ) ) _d x )
89 12 16 31 32 itgadd 
 |-  ( ph -> S. A ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) _d x = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) )
90 88 89 eqtr3d 
 |-  ( ph -> S. A ( Re ` ( C x. B ) ) _d x = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) )
91 85 9 immuld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) )
92 91 itgeq2dv 
 |-  ( ph -> S. A ( Im ` ( C x. B ) ) _d x = S. A ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) _d x )
93 21 23 36 37 itgadd 
 |-  ( ph -> S. A ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) _d x = ( S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x + S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
94 92 93 eqtrd 
 |-  ( ph -> S. A ( Im ` ( C x. B ) ) _d x = ( S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x + S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
95 94 oveq2d 
 |-  ( ph -> ( _i x. S. A ( Im ` ( C x. B ) ) _d x ) = ( _i x. ( S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x + S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) )
96 53 24 38 adddid 
 |-  ( ph -> ( _i x. ( S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x + S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) = ( ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) )
97 95 96 eqtrd 
 |-  ( ph -> ( _i x. S. A ( Im ` ( C x. B ) ) _d x ) = ( ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) )
98 90 97 oveq12d 
 |-  ( ph -> ( S. A ( Re ` ( C x. B ) ) _d x + ( _i x. S. A ( Im ` ( C x. B ) ) _d x ) ) = ( ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) + ( ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) + ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) ) ) )
99 41 80 98 3eqtr4d 
 |-  ( ph -> ( ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) x. S. A B _d x ) = ( S. A ( Re ` ( C x. B ) ) _d x + ( _i x. S. A ( Im ` ( C x. B ) ) _d x ) ) )
100 1 replimd 
 |-  ( ph -> C = ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) )
101 100 oveq1d 
 |-  ( ph -> ( C x. S. A B _d x ) = ( ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) x. S. A B _d x ) )
102 85 9 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. CC )
103 1 2 3 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. L^1 )
104 102 103 itgcnval 
 |-  ( ph -> S. A ( C x. B ) _d x = ( S. A ( Re ` ( C x. B ) ) _d x + ( _i x. S. A ( Im ` ( C x. B ) ) _d x ) ) )
105 99 101 104 3eqtr4d 
 |-  ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )