Metamath Proof Explorer

Theorem remullem

Description: Lemma for remul , immul , and cjmul . (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion remullem 
|- ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) /\ ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) /\ ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
2 replim 
 |-  ( B e. CC -> B = ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) )
3 1 2 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) )
4 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
5 4 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. RR )
6 5 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` A ) e. CC )
7 ax-icn 
 |-  _i e. CC
8 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
9 8 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. RR )
10 9 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` A ) e. CC )
11 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
12 7 10 11 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
13 6 12 addcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) e. CC )
14 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
15 14 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. RR )
16 15 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` B ) e. CC )
17 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
18 17 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. RR )
19 18 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` B ) e. CC )
20 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` B ) e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
21 7 19 20 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` B ) ) e. CC )
22 13 16 21 adddid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( ( Re ` B ) + ( _i x. ( Im ` B ) ) ) ) = ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( Re ` B ) ) + ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( _i x. ( Im ` B ) ) ) ) )
23 6 12 16 adddird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( Re ` B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) )
24 6 12 21 adddird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( _i x. ( Im ` B ) ) ) = ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) )
25 23 24 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( Re ` B ) ) + ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( _i x. ( Im ` B ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) + ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) ) )
26 5 15 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. RR )
27 26 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. CC )
28 12 21 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) e. CC )
29 12 16 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) e. CC )
30 6 21 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) e. CC )
31 27 28 29 30 add42d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) + ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) + ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) + ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) ) )
32 7 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i e. CC )
33 32 10 32 19 mul4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) = ( ( _i x. _i ) x. ( ( Im ` A ) x. ( Im ` B ) ) ) )
34 ixi 
 |-  ( _i x. _i ) = -u 1
35 34 oveq1i 
 |-  ( ( _i x. _i ) x. ( ( Im ` A ) x. ( Im ` B ) ) ) = ( -u 1 x. ( ( Im ` A ) x. ( Im ` B ) ) )
36 9 18 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. RR )
37 36 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. CC )
38 37 mulm1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( Im ` A ) x. ( Im ` B ) ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
39 35 38 eqtrid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( ( Im ` A ) x. ( Im ` B ) ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
40 33 39 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
41 40 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + -u ( ( Im ` A ) x. ( Im ` B ) ) ) )
42 27 37 negsubd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) + -u ( ( Im ` A ) x. ( Im ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
43 41 42 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
44 9 15 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Re ` B ) ) e. RR )
45 44 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Re ` B ) ) e. CC )
46 mulcl 
 |-  ( ( _i e. CC /\ ( ( Im ` A ) x. ( Re ` B ) ) e. CC ) -> ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) e. CC )
47 7 45 46 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) e. CC )
48 5 18 remulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Im ` B ) ) e. RR )
49 48 recnd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Im ` B ) ) e. CC )
50 mulcl 
 |-  ( ( _i e. CC /\ ( ( Re ` A ) x. ( Im ` B ) ) e. CC ) -> ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) e. CC )
51 7 49 50 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) e. CC )
52 47 51 addcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) + ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) ) = ( ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) ) )
53 32 10 16 mulassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) = ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) )
54 6 32 19 mul12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) = ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) )
55 53 54 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) + ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) = ( ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) + ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) ) )
56 32 49 45 adddid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) = ( ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) ) )
57 52 55 56 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) + ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) = ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) )
58 43 57 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) + ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) + ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) )
59 25 31 58 3eqtr2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( Re ` B ) ) + ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) x. ( _i x. ( Im ` B ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) )
60 3 22 59 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) )
61 60 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( Re ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) )
62 26 36 resubcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) e. RR )
63 48 44 readdcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) e. RR )
64 crre 
 |-  ( ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) e. RR /\ ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) e. RR ) -> ( Re ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
65 62 63 64 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
66 61 65 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
67 60 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( Im ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) )
68 crim 
 |-  ( ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) e. RR /\ ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) e. RR ) -> ( Im ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
69 62 63 68 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
70 67 69 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
71 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
72 remim 
 |-  ( ( A x. B ) e. CC -> ( * ` ( A x. B ) ) = ( ( Re ` ( A x. B ) ) - ( _i x. ( Im ` ( A x. B ) ) ) ) )
73 71 72 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( Re ` ( A x. B ) ) - ( _i x. ( Im ` ( A x. B ) ) ) ) )
74 remim 
 |-  ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
75 remim 
 |-  ( B e. CC -> ( * ` B ) = ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) )
76 74 75 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) x. ( * ` B ) ) = ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) )
77 16 21 subcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) e. CC )
78 6 12 77 subdird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) - ( ( _i x. ( Im ` A ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) ) )
79 27 30 29 28 subadd4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) - ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) - ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) - ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) ) )
80 6 16 21 subdid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) )
81 12 16 21 subdid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( Im ` A ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) = ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) - ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) )
82 80 81 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) - ( ( _i x. ( Im ` A ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) ) - ( ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) - ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) ) )
83 65 61 43 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) )
84 70 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` ( A x. B ) ) ) = ( _i x. ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) ) )
85 54 53 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) = ( ( _i x. ( ( Re ` A ) x. ( Im ` B ) ) ) + ( _i x. ( ( Im ` A ) x. ( Re ` B ) ) ) ) )
86 56 84 85 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( Im ` ( A x. B ) ) ) = ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) )
87 83 86 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A x. B ) ) - ( _i x. ( Im ` ( A x. B ) ) ) ) = ( ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( _i x. ( Im ` A ) ) x. ( _i x. ( Im ` B ) ) ) ) - ( ( ( Re ` A ) x. ( _i x. ( Im ` B ) ) ) + ( ( _i x. ( Im ` A ) ) x. ( Re ` B ) ) ) ) )
88 79 82 87 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) - ( ( _i x. ( Im ` A ) ) x. ( ( Re ` B ) - ( _i x. ( Im ` B ) ) ) ) ) = ( ( Re ` ( A x. B ) ) - ( _i x. ( Im ` ( A x. B ) ) ) ) )
89 76 78 88 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) x. ( * ` B ) ) = ( ( Re ` ( A x. B ) ) - ( _i x. ( Im ` ( A x. B ) ) ) ) )
90 73 89 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) )
91 66 70 90 3jca 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) /\ ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) /\ ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) ) )