Metamath Proof Explorer

Theorem cphipipcj

Description: An inner product times its conjugate. (Contributed by NM, 23-Nov-2007) (Revised by AV, 19-Oct-2021)

Ref Expression
Hypotheses cphipcj.h 
|- ., = ( .i ` W )
cphipcj.v 
|- V = ( Base ` W )
Assertion cphipipcj 
|- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) x. ( B ., A ) ) = ( ( abs ` ( A ., B ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h 
 |-  ., = ( .i ` W )
2 cphipcj.v 
 |-  V = ( Base ` W )
3 2 1 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )
4 absval 
 |-  ( ( A ., B ) e. CC -> ( abs ` ( A ., B ) ) = ( sqrt ` ( ( A ., B ) x. ( * ` ( A ., B ) ) ) ) )
5 3 4 syl 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( abs ` ( A ., B ) ) = ( sqrt ` ( ( A ., B ) x. ( * ` ( A ., B ) ) ) ) )
6 5 oveq1d 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( abs ` ( A ., B ) ) ^ 2 ) = ( ( sqrt ` ( ( A ., B ) x. ( * ` ( A ., B ) ) ) ) ^ 2 ) )
7 3 cjcld 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( * ` ( A ., B ) ) e. CC )
8 3 7 mulcld 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) x. ( * ` ( A ., B ) ) ) e. CC )
9 8 sqsqrtd 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( sqrt ` ( ( A ., B ) x. ( * ` ( A ., B ) ) ) ) ^ 2 ) = ( ( A ., B ) x. ( * ` ( A ., B ) ) ) )
10 1 2 cphipcj 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( * ` ( A ., B ) ) = ( B ., A ) )
11 10 oveq2d 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) x. ( * ` ( A ., B ) ) ) = ( ( A ., B ) x. ( B ., A ) ) )
12 6 9 11 3eqtrrd 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) x. ( B ., A ) ) = ( ( abs ` ( A ., B ) ) ^ 2 ) )