Metamath Proof Explorer


Theorem immul2d

Description: Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses crred.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
remul2d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
Assertion immul2d ( ๐œ‘ โ†’ ( โ„‘ โ€˜ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ„‘ โ€˜ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 crred.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 remul2d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
3 immul2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( โ„‘ โ€˜ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ„‘ โ€˜ ๐ต ) ) )
4 1 2 3 syl2anc โŠข ( ๐œ‘ โ†’ ( โ„‘ โ€˜ ( ๐ด ยท ๐ต ) ) = ( ๐ด ยท ( โ„‘ โ€˜ ๐ต ) ) )