Step |
Hyp |
Ref |
Expression |
1 |
|
mbfmulc2.1 |
|- ( ph -> C e. CC ) |
2 |
|
mbfmulc2.2 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
3 |
|
mbfmulc2.3 |
|- ( ph -> ( x e. A |-> B ) e. MblFn ) |
4 |
3 2
|
mbfdm2 |
|- ( ph -> A e. dom vol ) |
5 |
1
|
recld |
|- ( ph -> ( Re ` C ) e. RR ) |
6 |
5
|
adantr |
|- ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR ) |
7 |
6
|
recnd |
|- ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC ) |
8 |
3 2
|
mbfmptcl |
|- ( ( ph /\ x e. A ) -> B e. CC ) |
9 |
8
|
recld |
|- ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR ) |
10 |
9
|
recnd |
|- ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC ) |
11 |
7 10
|
mulcld |
|- ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Re ` B ) ) e. CC ) |
12 |
|
ovexd |
|- ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) e. _V ) |
13 |
|
fconstmpt |
|- ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) ) |
14 |
13
|
a1i |
|- ( ph -> ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) ) ) |
15 |
|
eqidd |
|- ( ph -> ( x e. A |-> ( Re ` B ) ) = ( x e. A |-> ( Re ` B ) ) ) |
16 |
4 6 9 14 15
|
offval2 |
|- ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) ) |
17 |
1
|
imcld |
|- ( ph -> ( Im ` C ) e. RR ) |
18 |
17
|
renegcld |
|- ( ph -> -u ( Im ` C ) e. RR ) |
19 |
18
|
adantr |
|- ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. RR ) |
20 |
8
|
imcld |
|- ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR ) |
21 |
|
fconstmpt |
|- ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) ) |
22 |
21
|
a1i |
|- ( ph -> ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) ) ) |
23 |
|
eqidd |
|- ( ph -> ( x e. A |-> ( Im ` B ) ) = ( x e. A |-> ( Im ` B ) ) ) |
24 |
4 19 20 22 23
|
offval2 |
|- ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) ) |
25 |
4 11 12 16 24
|
offval2 |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) ) ) |
26 |
17
|
adantr |
|- ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR ) |
27 |
26
|
recnd |
|- ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC ) |
28 |
20
|
recnd |
|- ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC ) |
29 |
27 28
|
mulcld |
|- ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Im ` B ) ) e. CC ) |
30 |
11 29
|
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 ) ) ) ) |
31 |
27 28
|
mulneg1d |
|- ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) = -u ( ( Im ` C ) x. ( Im ` B ) ) ) |
32 |
31
|
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 ) ) ) ) |
33 |
1
|
adantr |
|- ( ( ph /\ x e. A ) -> C e. CC ) |
34 |
33 8
|
remuld |
|- ( ( ph /\ x e. A ) -> ( Re ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) ) |
35 |
30 32 34
|
3eqtr4d |
|- ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) = ( Re ` ( C x. B ) ) ) |
36 |
35
|
mpteq2dva |
|- ( ph -> ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) ) = ( x e. A |-> ( Re ` ( C x. B ) ) ) ) |
37 |
25 36
|
eqtrd |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) = ( x e. A |-> ( Re ` ( C x. B ) ) ) ) |
38 |
8
|
ismbfcn2 |
|- ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) ) |
39 |
3 38
|
mpbid |
|- ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) |
40 |
39
|
simpld |
|- ( ph -> ( x e. A |-> ( Re ` B ) ) e. MblFn ) |
41 |
10
|
fmpttd |
|- ( ph -> ( x e. A |-> ( Re ` B ) ) : A --> CC ) |
42 |
40 5 41
|
mbfmulc2re |
|- ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn ) |
43 |
39
|
simprd |
|- ( ph -> ( x e. A |-> ( Im ` B ) ) e. MblFn ) |
44 |
28
|
fmpttd |
|- ( ph -> ( x e. A |-> ( Im ` B ) ) : A --> CC ) |
45 |
43 18 44
|
mbfmulc2re |
|- ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn ) |
46 |
42 45
|
mbfadd |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) e. MblFn ) |
47 |
37 46
|
eqeltrrd |
|- ( ph -> ( x e. A |-> ( Re ` ( C x. B ) ) ) e. MblFn ) |
48 |
|
ovexd |
|- ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Im ` B ) ) e. _V ) |
49 |
|
ovexd |
|- ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Re ` B ) ) e. _V ) |
50 |
4 6 20 14 23
|
offval2 |
|- ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) ) |
51 |
|
fconstmpt |
|- ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) ) |
52 |
51
|
a1i |
|- ( ph -> ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) ) ) |
53 |
4 26 9 52 15
|
offval2 |
|- ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) ) |
54 |
4 48 49 50 53
|
offval2 |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) ) |
55 |
33 8
|
immuld |
|- ( ( ph /\ x e. A ) -> ( Im ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) |
56 |
55
|
mpteq2dva |
|- ( ph -> ( x e. A |-> ( Im ` ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) ) |
57 |
54 56
|
eqtr4d |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) = ( x e. A |-> ( Im ` ( C x. B ) ) ) ) |
58 |
43 5 44
|
mbfmulc2re |
|- ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn ) |
59 |
40 17 41
|
mbfmulc2re |
|- ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn ) |
60 |
58 59
|
mbfadd |
|- ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) e. MblFn ) |
61 |
57 60
|
eqeltrrd |
|- ( ph -> ( x e. A |-> ( Im ` ( C x. B ) ) ) e. MblFn ) |
62 |
33 8
|
mulcld |
|- ( ( ph /\ x e. A ) -> ( C x. B ) e. CC ) |
63 |
62
|
ismbfcn2 |
|- ( ph -> ( ( x e. A |-> ( C x. B ) ) e. MblFn <-> ( ( x e. A |-> ( Re ` ( C x. B ) ) ) e. MblFn /\ ( x e. A |-> ( Im ` ( C x. B ) ) ) e. MblFn ) ) ) |
64 |
47 61 63
|
mpbir2and |
|- ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn ) |