Description: Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | crred.1 | โข ( ๐ โ ๐ด โ โ ) | |
remul2d.2 | โข ( ๐ โ ๐ต โ โ ) | ||
Assertion | immul2d | โข ( ๐ โ ( โ โ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ โ ๐ต ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crred.1 | โข ( ๐ โ ๐ด โ โ ) | |
2 | remul2d.2 | โข ( ๐ โ ๐ต โ โ ) | |
3 | immul2 | โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( โ โ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ โ ๐ต ) ) ) | |
4 | 1 2 3 | syl2anc | โข ( ๐ โ ( โ โ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ โ ๐ต ) ) ) |