Theorem cphnmcl

Description: The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-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)$$
	cphnmcl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cphnmcl.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphnmcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to N\left(A\right)\in K$$

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		cphnmcl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		cphnmcl.k	$$⊢K={\mathrm{Base}}_F$$
6	1 2 3 4 5	cphnmf	$$⊢W\in \mathrm{CPreHil}\to N:V⟶K$$
7	6	ffvelrnda	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to N\left(A\right)\in K$$