Metamath Proof Explorer

Theorem ipcnval

Description: Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion ipcnval 
|- ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 cjcl 
 |-  ( B e. CC -> ( * ` B ) e. CC )
2 remul 
 |-  ( ( A e. CC /\ ( * ` B ) e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` ( * ` B ) ) ) - ( ( Im ` A ) x. ( Im ` ( * ` B ) ) ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` ( * ` B ) ) ) - ( ( Im ` A ) x. ( Im ` ( * ` B ) ) ) ) )
4 recj 
 |-  ( B e. CC -> ( Re ` ( * ` B ) ) = ( Re ` B ) )
5 4 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( * ` B ) ) = ( Re ` B ) )
6 5 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Re ` ( * ` B ) ) ) = ( ( Re ` A ) x. ( Re ` B ) ) )
7 imcj 
 |-  ( B e. CC -> ( Im ` ( * ` B ) ) = -u ( Im ` B ) )
8 7 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( * ` B ) ) = -u ( Im ` B ) )
9 8 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Im ` ( * ` B ) ) ) = ( ( Im ` A ) x. -u ( Im ` 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 mulneg2 
 |-  ( ( ( Im ` A ) e. CC /\ ( Im ` B ) e. CC ) -> ( ( Im ` A ) x. -u ( Im ` B ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
15 11 13 14 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. -u ( Im ` B ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
16 9 15 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Im ` ( * ` B ) ) ) = -u ( ( Im ` A ) x. ( Im ` B ) ) )
17 6 16 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` ( * ` B ) ) ) - ( ( Im ` A ) x. ( Im ` ( * ` B ) ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - -u ( ( Im ` A ) x. ( Im ` B ) ) ) )
18 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
19 18 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
20 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
21 20 recnd 
 |-  ( B e. CC -> ( Re ` B ) e. CC )
22 mulcl 
 |-  ( ( ( Re ` A ) e. CC /\ ( Re ` B ) e. CC ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. CC )
23 19 21 22 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Re ` A ) x. ( Re ` B ) ) e. CC )
24 mulcl 
 |-  ( ( ( Im ` A ) e. CC /\ ( Im ` B ) e. CC ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. CC )
25 11 13 24 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( Im ` A ) x. ( Im ` B ) ) e. CC )
26 23 25 subnegd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( Re ` A ) x. ( Re ` B ) ) - -u ( ( Im ` A ) x. ( Im ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) ) )
27 3 17 26 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) ) )