This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐾 )