This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipipcj

Description: An inner product times its conjugate. (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 
|- X = ( BaseSet ` U )
ipcl.7 
|- P = ( .iOLD ` U )
Assertion ipipcj 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 ipcl.1 
 |-  X = ( BaseSet ` U )
2 ipcl.7 
 |-  P = ( .iOLD ` U )
3 1 2 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )
4 3 absvalsqd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( abs ` ( A P B ) ) ^ 2 ) = ( ( A P B ) x. ( * ` ( A P B ) ) ) )
5 1 2 dipcj 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) )
6 5 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( * ` ( A P B ) ) ) = ( ( A P B ) x. ( B P A ) ) )
7 4 6 eqtr2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) x. ( B P A ) ) = ( ( abs ` ( A P B ) ) ^ 2 ) )