Metamath Proof Explorer

Theorem cjreim

Description: The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005)

Ref Expression
Assertion cjreim 
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( A - ( _i x. B ) ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 ax-icn 
 |-  _i e. CC
3 recn 
 |-  ( B e. RR -> B e. CC )
4 mulcl 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
5 2 3 4 sylancr 
 |-  ( B e. RR -> ( _i x. B ) e. CC )
6 cjadd 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( * ` ( A + ( _i x. B ) ) ) = ( ( * ` A ) + ( * ` ( _i x. B ) ) ) )
7 1 5 6 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( ( * ` A ) + ( * ` ( _i x. B ) ) ) )
8 cjre 
 |-  ( A e. RR -> ( * ` A ) = A )
9 cjmul 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( * ` ( _i x. B ) ) = ( ( * ` _i ) x. ( * ` B ) ) )
10 2 3 9 sylancr 
 |-  ( B e. RR -> ( * ` ( _i x. B ) ) = ( ( * ` _i ) x. ( * ` B ) ) )
11 cji 
 |-  ( * ` _i ) = -u _i
12 11 a1i 
 |-  ( B e. RR -> ( * ` _i ) = -u _i )
13 cjre 
 |-  ( B e. RR -> ( * ` B ) = B )
14 12 13 oveq12d 
 |-  ( B e. RR -> ( ( * ` _i ) x. ( * ` B ) ) = ( -u _i x. B ) )
15 mulneg1 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( -u _i x. B ) = -u ( _i x. B ) )
16 2 3 15 sylancr 
 |-  ( B e. RR -> ( -u _i x. B ) = -u ( _i x. B ) )
17 10 14 16 3eqtrd 
 |-  ( B e. RR -> ( * ` ( _i x. B ) ) = -u ( _i x. B ) )
18 8 17 oveqan12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( * ` A ) + ( * ` ( _i x. B ) ) ) = ( A + -u ( _i x. B ) ) )
19 negsub 
 |-  ( ( A e. CC /\ ( _i x. B ) e. CC ) -> ( A + -u ( _i x. B ) ) = ( A - ( _i x. B ) ) )
20 1 5 19 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + -u ( _i x. B ) ) = ( A - ( _i x. B ) ) )
21 7 18 20 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( A - ( _i x. B ) ) )