Theorem 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{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	cphipipcj	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B\right)\left(B\underset{\dot{}}{,}A\right)={\left|A\underset{\dot{}}{,}B\right|}^2$$

Proof

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