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	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	cphipcj.v	$⊢ V = {Base}_{W}$
Assertion	cphipipcj	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to (A \underset{˙}{,} B) (B \underset{˙}{,} A) = {\|A \underset{˙}{,} B\|}^{2}$

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3	2 1	cphipcl	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to A \underset{˙}{,} B \in ℂ$
4		absval	$⊢ A \underset{˙}{,} B \in ℂ \to \|A \underset{˙}{,} B\| = \sqrt{(A \underset{˙}{,} B) \overline{A \underset{˙}{,} B}}$
5	3 4	syl	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \|A \underset{˙}{,} B\| = \sqrt{(A \underset{˙}{,} B) \overline{A \underset{˙}{,} B}}$
6	5	oveq1d	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to {\|A \underset{˙}{,} B\|}^{2} = {\sqrt{(A \underset{˙}{,} B) \overline{A \underset{˙}{,} B}}}^{2}$
7	3	cjcld	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \overline{A \underset{˙}{,} B} \in ℂ$
8	3 7	mulcld	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to (A \underset{˙}{,} B) \overline{A \underset{˙}{,} B} \in ℂ$
9	8	sqsqrtd	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to {\sqrt{(A \underset{˙}{,} B) \overline{A \underset{˙}{,} B}}}^{2} = (A \underset{˙}{,} B) \overline{A \underset{˙}{,} B}$
10	1 2	cphipcj	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \overline{A \underset{˙}{,} B} = B \underset{˙}{,} A$
11	10	oveq2d	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to (A \underset{˙}{,} B) \overline{A \underset{˙}{,} B} = (A \underset{˙}{,} B) (B \underset{˙}{,} A)$
12	6 9 11	3eqtrrd	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to (A \underset{˙}{,} B) (B \underset{˙}{,} A) = {\|A \underset{˙}{,} B\|}^{2}$

Metamath Proof Explorer