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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	nmsq.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	nmsq.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	cphnmcl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphnmcl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cphnmcl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		nmsq.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		nmsq.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		nmsq.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
4		cphnmcl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		cphnmcl.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6	1 2 3 4 5	cphnmf	⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 : 𝑉 ⟶ 𝐾 )
7	6	ffvelcdmda	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐾 )