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 ) ) ) )