Metamath Proof Explorer

Theorem itgmulc2nc

Description: Choice-free analogue of itgmulc2 . (Contributed by Brendan Leahy, 19-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 
 |-  ( ph -> C e. CC )
2 itgmulc2nc.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 itgmulc2nc.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 itgmulc2nc.m 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )
5 1 recld 
 |-  ( ph -> ( Re ` C ) e. RR )
6 5 recnd 
 |-  ( ph -> ( Re ` C ) e. CC )
7 6 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC )
8 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
9 3 8 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
10 9 2 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
11 10 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
12 11 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
13 7 12 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Re ` B ) ) e. CC )
14 10 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 ) ) )
15 3 14 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
16 15 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
17 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. _V )
18 4 17 mbfdm2 
 |-  ( ph -> A e. dom vol )
19 fconstmpt 
 |-  ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) )
20 19 a1i 
 |-  ( ph -> ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) ) )
21 eqidd 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) = ( x e. A |-> ( Re ` B ) ) )
22 18 7 11 20 21 offval2 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) )
23 iblmbf 
 |-  ( ( x e. A |-> ( Re ` B ) ) e. L^1 -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
24 16 23 syl 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
25 12 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) : A --> CC )
26 24 5 25 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn )
27 22 26 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) e. MblFn )
28 6 11 16 27 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) e. L^1 )
29 13 28 itgcl 
 |-  ( ph -> S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x e. CC )
30 ax-icn 
 |-  _i e. CC
31 10 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
32 31 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
33 7 32 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Im ` B ) ) e. CC )
34 15 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
35 eqidd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) = ( x e. A |-> ( Im ` B ) ) )
36 18 7 31 20 35 offval2 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) )
37 iblmbf 
 |-  ( ( x e. A |-> ( Im ` B ) ) e. L^1 -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
38 34 37 syl 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
39 32 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) : A --> CC )
40 38 5 39 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn )
41 36 40 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) e. MblFn )
42 6 31 34 41 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) e. L^1 )
43 33 42 itgcl 
 |-  ( ph -> S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x e. CC )
44 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 )
45 30 43 44 sylancr 
 |-  ( ph -> ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) e. CC )
46 1 imcld 
 |-  ( ph -> ( Im ` C ) e. RR )
47 46 recnd 
 |-  ( ph -> ( Im ` C ) e. CC )
48 47 negcld 
 |-  ( ph -> -u ( Im ` C ) e. CC )
49 48 adantr 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. CC )
50 49 32 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) e. CC )
51 fconstmpt 
 |-  ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) )
52 51 a1i 
 |-  ( ph -> ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) ) )
53 18 49 31 52 35 offval2 
 |-  ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) )
54 46 renegcld 
 |-  ( ph -> -u ( Im ` C ) e. RR )
55 38 54 39 mbfmulc2re 
 |-  ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn )
56 53 55 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) e. MblFn )
57 48 31 34 56 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) e. L^1 )
58 50 57 itgcl 
 |-  ( ph -> S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x e. CC )
59 47 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC )
60 59 12 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Re ` B ) ) e. CC )
61 fconstmpt 
 |-  ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) )
62 61 a1i 
 |-  ( ph -> ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) ) )
63 18 59 11 62 21 offval2 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) )
64 24 46 25 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn )
65 63 64 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) e. MblFn )
66 47 11 16 65 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) e. L^1 )
67 60 66 itgcl 
 |-  ( ph -> S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x e. CC )
68 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 )
69 30 67 68 sylancr 
 |-  ( ph -> ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) e. CC )
70 29 45 58 69 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 ) ) ) )
71 30 a1i 
 |-  ( ph -> _i e. CC )
72 71 47 mulcld 
 |-  ( ph -> ( _i x. ( Im ` C ) ) e. CC )
73 2 3 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
74 6 72 73 adddird 
 |-  ( ph -> ( ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) x. S. A B _d x ) = ( ( ( Re ` C ) x. S. A B _d x ) + ( ( _i x. ( Im ` C ) ) x. S. A B _d x ) ) )
75 2 3 itgcnval 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
76 75 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 ) ) ) )
77 11 16 itgcl 
 |-  ( ph -> S. A ( Re ` B ) _d x e. CC )
78 31 34 itgcl 
 |-  ( ph -> S. A ( Im ` B ) _d x e. CC )
79 mulcl 
 |-  ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
80 30 78 79 sylancr 
 |-  ( ph -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
81 6 77 80 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 ) ) ) )
82 6 11 16 27 5 11 itgmulc2nclem2 
 |-  ( ph -> ( ( Re ` C ) x. S. A ( Re ` B ) _d x ) = S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x )
83 6 71 78 mul12d 
 |-  ( ph -> ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = ( _i x. ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) ) )
84 6 31 34 41 5 31 itgmulc2nclem2 
 |-  ( ph -> ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x )
85 84 oveq2d 
 |-  ( ph -> ( _i x. ( ( Re ` C ) x. S. A ( Im ` B ) _d x ) ) = ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) )
86 83 85 eqtrd 
 |-  ( ph -> ( ( Re ` C ) x. ( _i x. S. A ( Im ` B ) _d x ) ) = ( _i x. S. A ( ( Re ` C ) x. ( Im ` B ) ) _d x ) )
87 82 86 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 ) ) )
88 76 81 87 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 ) ) )
89 75 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 ) ) ) )
90 72 77 80 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 ) ) ) )
91 71 47 77 mulassd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) = ( _i x. ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) ) )
92 47 11 16 65 46 11 itgmulc2nclem2 
 |-  ( ph -> ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) = S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x )
93 92 oveq2d 
 |-  ( ph -> ( _i x. ( ( Im ` C ) x. S. A ( Re ` B ) _d x ) ) = ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
94 91 93 eqtrd 
 |-  ( ph -> ( ( _i x. ( Im ` C ) ) x. S. A ( Re ` B ) _d x ) = ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) )
95 71 47 71 78 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 ) ) )
96 ixi 
 |-  ( _i x. _i ) = -u 1
97 96 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 ) )
98 47 78 mulcld 
 |-  ( ph -> ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) e. CC )
99 98 mulm1d 
 |-  ( ph -> ( -u 1 x. ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) ) = -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
100 97 99 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 ) )
101 47 78 mulneg1d 
 |-  ( ph -> ( -u ( Im ` C ) x. S. A ( Im ` B ) _d x ) = -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) )
102 48 31 34 56 54 31 itgmulc2nclem2 
 |-  ( ph -> ( -u ( Im ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
103 101 102 eqtr3d 
 |-  ( ph -> -u ( ( Im ` C ) x. S. A ( Im ` B ) _d x ) = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
104 95 100 103 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 )
105 94 104 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 ) )
106 69 58 addcomd 
 |-  ( ph -> ( ( _i x. S. A ( ( Im ` C ) x. ( Re ` B ) ) _d x ) + S. A ( -u ( Im ` 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 ) ) )
107 105 106 eqtrd 
 |-  ( 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 ) ) )
108 89 90 107 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 ) ) )
109 88 108 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 ) ) ) )
110 74 109 eqtrd 
 |-  ( 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 ) ) ) )
111 59 32 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Im ` B ) ) e. CC )
112 18 59 31 62 35 offval2 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( ( Im ` C ) x. ( Im ` B ) ) ) )
113 38 46 39 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn )
114 112 113 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Im ` C ) x. ( Im ` B ) ) ) e. MblFn )
115 47 31 34 114 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( ( Im ` C ) x. ( Im ` B ) ) ) e. L^1 )
116 1 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
117 116 10 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. CC )
118 eqidd 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) = ( x e. A |-> ( C x. B ) ) )
119 ref 
 |-  Re : CC --> RR
120 119 a1i 
 |-  ( ph -> Re : CC --> RR )
121 120 feqmptd 
 |-  ( ph -> Re = ( k e. CC |-> ( Re ` k ) ) )
122 fveq2 
 |-  ( k = ( C x. B ) -> ( Re ` k ) = ( Re ` ( C x. B ) ) )
123 117 118 121 122 fmptco 
 |-  ( ph -> ( Re o. ( x e. A |-> ( C x. B ) ) ) = ( x e. A |-> ( Re ` ( C x. B ) ) ) )
124 116 10 remuld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) )
125 124 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Re ` ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) ) )
126 123 125 eqtrd 
 |-  ( ph -> ( Re o. ( x e. A |-> ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) ) )
127 117 fmpttd 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) : A --> CC )
128 ismbfcn 
 |-  ( ( x e. A |-> ( C x. B ) ) : A --> CC -> ( ( x e. A |-> ( C x. B ) ) e. MblFn <-> ( ( Re o. ( x e. A |-> ( C x. B ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( C x. B ) ) ) e. MblFn ) ) )
129 127 128 syl 
 |-  ( ph -> ( ( x e. A |-> ( C x. B ) ) e. MblFn <-> ( ( Re o. ( x e. A |-> ( C x. B ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( C x. B ) ) ) e. MblFn ) ) )
130 4 129 mpbid 
 |-  ( ph -> ( ( Re o. ( x e. A |-> ( C x. B ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( C x. B ) ) ) e. MblFn ) )
131 130 simpld 
 |-  ( ph -> ( Re o. ( x e. A |-> ( C x. B ) ) ) e. MblFn )
132 126 131 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) ) e. MblFn )
133 13 28 111 115 132 itgsubnc 
 |-  ( ph -> S. A ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) _d x = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x - S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x ) )
134 124 itgeq2dv 
 |-  ( ph -> S. A ( Re ` ( C x. B ) ) _d x = S. A ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) _d x )
135 111 115 itgneg 
 |-  ( ph -> -u S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x = S. A -u ( ( Im ` C ) x. ( Im ` B ) ) _d x )
136 59 32 mulneg1d 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) = -u ( ( Im ` C ) x. ( Im ` B ) ) )
137 136 itgeq2dv 
 |-  ( ph -> S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x = S. A -u ( ( Im ` C ) x. ( Im ` B ) ) _d x )
138 135 137 eqtr4d 
 |-  ( ph -> -u S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x = S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x )
139 138 oveq2d 
 |-  ( ph -> ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + -u S. A ( ( 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 ) )
140 111 115 itgcl 
 |-  ( ph -> S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x e. CC )
141 29 140 negsubd 
 |-  ( ph -> ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + -u S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x ) = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x - S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x ) )
142 139 141 eqtr3d 
 |-  ( ph -> ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x + S. A ( -u ( Im ` C ) x. ( Im ` B ) ) _d x ) = ( S. A ( ( Re ` C ) x. ( Re ` B ) ) _d x - S. A ( ( Im ` C ) x. ( Im ` B ) ) _d x ) )
143 133 134 142 3eqtr4d 
 |-  ( 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 ) )
144 116 10 immuld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) )
145 144 itgeq2dv 
 |-  ( ph -> S. A ( Im ` ( C x. B ) ) _d x = S. A ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) _d x )
146 imf 
 |-  Im : CC --> RR
147 146 a1i 
 |-  ( ph -> Im : CC --> RR )
148 147 feqmptd 
 |-  ( ph -> Im = ( k e. CC |-> ( Im ` k ) ) )
149 fveq2 
 |-  ( k = ( C x. B ) -> ( Im ` k ) = ( Im ` ( C x. B ) ) )
150 117 118 148 149 fmptco 
 |-  ( ph -> ( Im o. ( x e. A |-> ( C x. B ) ) ) = ( x e. A |-> ( Im ` ( C x. B ) ) ) )
151 144 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Im ` ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) )
152 150 151 eqtrd 
 |-  ( ph -> ( Im o. ( x e. A |-> ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) )
153 130 simprd 
 |-  ( ph -> ( Im o. ( x e. A |-> ( C x. B ) ) ) e. MblFn )
154 152 153 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) e. MblFn )
155 33 42 60 66 154 itgaddnc 
 |-  ( 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 ) )
156 145 155 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 ) )
157 156 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 ) ) )
158 71 43 67 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 ) ) )
159 157 158 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 ) ) )
160 143 159 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 ) ) ) )
161 70 110 160 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 ) ) )
162 1 replimd 
 |-  ( ph -> C = ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) )
163 162 oveq1d 
 |-  ( ph -> ( C x. S. A B _d x ) = ( ( ( Re ` C ) + ( _i x. ( Im ` C ) ) ) x. S. A B _d x ) )
164 1 2 3 4 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. L^1 )
165 117 164 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 ) ) )
166 161 163 165 3eqtr4d 
 |-  ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )