Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cjmul | |- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 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 ) ) ) ) |
|
| 2 | 1 | simp3d | |- ( ( A e. CC /\ B e. CC ) -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) ) |