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 = ( Base ` W )
	nmsq.h	|- ., = ( .i ` W )
	nmsq.n	|- N = ( norm ` W )
	cphnmcl.f	|- F = ( Scalar ` W )
	cphnmcl.k	|- K = ( Base ` F )
Assertion	cphnmcl	|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) e. K )

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	|- V = ( Base ` W )
2		nmsq.h	|- ., = ( .i ` W )
3		nmsq.n	|- N = ( norm ` W )
4		cphnmcl.f	|- F = ( Scalar ` W )
5		cphnmcl.k	|- K = ( Base ` F )
6	1 2 3 4 5	cphnmf	|- ( W e. CPreHil -> N : V --> K )
7	6	ffvelrnda	|- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) e. K )