Theorem immul2

Description: Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	immul2	|- ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2		immul	|- ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
3	1 2	sylan	|- ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
4		rere	|- ( A e. RR -> ( Re ` A ) = A )
5	4	adantr	|- ( ( A e. RR /\ B e. CC ) -> ( Re ` A ) = A )
6	5	oveq1d	|- ( ( A e. RR /\ B e. CC ) -> ( ( Re ` A ) x. ( Im ` B ) ) = ( A x. ( Im ` B ) ) )
7		reim0	|- ( A e. RR -> ( Im ` A ) = 0 )
8	7	oveq1d	|- ( A e. RR -> ( ( Im ` A ) x. ( Re ` B ) ) = ( 0 x. ( Re ` B ) ) )
9		recl	|- ( B e. CC -> ( Re ` B ) e. RR )
10	9	recnd	|- ( B e. CC -> ( Re ` B ) e. CC )
11	10	mul02d	|- ( B e. CC -> ( 0 x. ( Re ` B ) ) = 0 )
12	8 11	sylan9eq	|- ( ( A e. RR /\ B e. CC ) -> ( ( Im ` A ) x. ( Re ` B ) ) = 0 )
13	6 12	oveq12d	|- ( ( A e. RR /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) = ( ( A x. ( Im ` B ) ) + 0 ) )
14		imcl	|- ( B e. CC -> ( Im ` B ) e. RR )
15	14	recnd	|- ( B e. CC -> ( Im ` B ) e. CC )
16		mulcl	|- ( ( A e. CC /\ ( Im ` B ) e. CC ) -> ( A x. ( Im ` B ) ) e. CC )
17	1 15 16	syl2an	|- ( ( A e. RR /\ B e. CC ) -> ( A x. ( Im ` B ) ) e. CC )
18	17	addid1d	|- ( ( A e. RR /\ B e. CC ) -> ( ( A x. ( Im ` B ) ) + 0 ) = ( A x. ( Im ` B ) ) )
19	3 13 18	3eqtrd	|- ( ( A e. RR /\ B e. CC ) -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )