Metamath Proof Explorer

Theorem cjsub

Description: Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 cjadd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( * ` ( A + -u B ) ) = ( ( * ` A ) + ( * ` -u B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + -u B ) ) = ( ( * ` A ) + ( * ` -u B ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A + -u B ) ) = ( * ` ( A - B ) ) )
6 cjneg 
 |-  ( B e. CC -> ( * ` -u B ) = -u ( * ` B ) )
7 6 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` -u B ) = -u ( * ` B ) )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) + ( * ` -u B ) ) = ( ( * ` A ) + -u ( * ` B ) ) )
9 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
10 cjcl 
 |-  ( B e. CC -> ( * ` B ) e. CC )
11 negsub 
 |-  ( ( ( * ` A ) e. CC /\ ( * ` B ) e. CC ) -> ( ( * ` A ) + -u ( * ` B ) ) = ( ( * ` A ) - ( * ` B ) ) )
12 9 10 11 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) + -u ( * ` B ) ) = ( ( * ` A ) - ( * ` B ) ) )
13 8 12 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) + ( * ` -u B ) ) = ( ( * ` A ) - ( * ` B ) ) )
14 3 5 13 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( * ` ( A - B ) ) = ( ( * ` A ) - ( * ` B ) ) )