Theorem cphnmfval

Description: The value of the norm in a subcomplex pre-Hilbert space is the square root of the inner product of a vector with itself. (Contributed 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	cphnmfval	$$⊢W\in \mathrm{CPreHil}\to N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$

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		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
6	1 2 3 4 5	iscph	$$⊢W\in \mathrm{CPreHil}\leftrightarrow \left(\left(W\in \mathrm{PreHil}\wedge W\in \mathrm{NrmMod}\wedge \mathrm{Scalar}\left(W\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\wedge \surd \left[{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)\right)$$
7	6	simp3bi	$$⊢W\in \mathrm{CPreHil}\to N=\left(x\in V⟼\sqrt{x\underset{\dot{}}{,}x}\right)$$