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 = \cdot_{𝑖OLD} (U)$
Assertion	ipipcj	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B) (B P A) = {\|A P B\|}^{2}$

Step	Hyp	Ref	Expression
1		ipcl.1	$⊢ X = BaseSet (U)$
2		ipcl.7	$⊢ P = \cdot_{𝑖OLD} (U)$
3	1 2	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
4	3	absvalsqd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to {\|A P B\|}^{2} = (A P B) \overline{A P B}$
5	1 2	dipcj	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \overline{A P B} = B P A$
6	5	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B) \overline{A P B} = (A P B) (B P A)$
7	4 6	eqtr2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B) (B P A) = {\|A P B\|}^{2}$

Metamath Proof Explorer