Metamath Proof Explorer

Theorem imsub

Description: Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005)

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

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 imadd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( Im ` ( A + -u B ) ) = ( ( Im ` A ) + ( Im ` -u B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + -u B ) ) = ( ( Im ` A ) + ( Im ` -u B ) ) )
4 imneg 
 |-  ( B e. CC -> ( Im ` -u B ) = -u ( Im ` B ) )
5 4 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` -u B ) = -u ( Im ` B ) )
6 5 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) + ( Im ` -u B ) ) = ( ( Im ` A ) + -u ( Im ` B ) ) )
7 3 6 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + -u B ) ) = ( ( Im ` A ) + -u ( Im ` B ) ) )
8 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
9 8 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + -u B ) ) = ( Im ` ( A - B ) ) )
10 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
11 10 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
12 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
13 12 recnd 
 |-  ( B e. CC -> ( Im ` B ) e. CC )
14 negsub 
 |-  ( ( ( Im ` A ) e. CC /\ ( Im ` B ) e. CC ) -> ( ( Im ` A ) + -u ( Im ` B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
15 11 13 14 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) + -u ( Im ` B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
16 7 9 15 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )