Theorem nmsq

Description: The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmsq.v	$$⊢V={\mathrm{Base}}_W$$
	nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	nmsq.n	$$⊢N=\mathrm{norm}\left(W\right)$$
Assertion	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	$$⊢V={\mathrm{Base}}_W$$
2		nmsq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		nmsq.n	$$⊢N=\mathrm{norm}\left(W\right)$$
4	1 2 3	cphnm	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to N\left(A\right)=\sqrt{A\underset{\dot{}}{,}A}$$
5	4	oveq1d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2={\sqrt{A\underset{\dot{}}{,}A}}^2$$
6	1 2	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℂ$$
7	6	3anidm23	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℂ$$
8	7	sqsqrtd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {\sqrt{A\underset{\dot{}}{,}A}}^2=A\underset{\dot{}}{,}A$$
9	5 8	eqtrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$