hlipcj

Description: Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlipf.1	$⊢ X = BaseSet (U)$
	hlipf.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	hlipcj	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to A P B = \overline{B P A}$

Step	Hyp	Ref	Expression
1		hlipf.1	$⊢ X = BaseSet (U)$
2		hlipf.7	$⊢ P = \cdot_{𝑖OLD} (U)$
3		hlnv	$⊢ U \in {CHil}_{OLD} \to U \in NrmCVec$
4	1 2	dipcj	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to \overline{B P A} = A P B$
5	3 4	syl3an1	$⊢ (U \in {CHil}_{OLD} \land B \in X \land A \in X) \to \overline{B P A} = A P B$
6	5	3com23	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to \overline{B P A} = A P B$
7	6	eqcomd	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to A P B = \overline{B P A}$

Metamath Proof Explorer