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 ) )