Metamath Proof Explorer

Theorem cphnmf

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 cphnmf ( 𝑊 ∈ ℂ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 cphnmfval ⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
7 simpl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ ℂPreHil )
8 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
9 8 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → 𝑊 ∈ PreHil )
10 simpr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
11 4 2 1 5 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 , 𝑥 ) ∈ 𝐾 )
12 9 10 10 11 syl3anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 , 𝑥 ) ∈ 𝐾 )
13 1 2 3 nmsq ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 , 𝑥 ) )
14 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
15 1 3 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑥 ) ∈ ℝ )
16 14 15 sylan ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑥 ) ∈ ℝ )
17 16 resqcld ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) ∈ ℝ )
18 13 17 eqeltrrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 , 𝑥 ) ∈ ℝ )
19 16 sqge0d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( ( 𝑁 ‘ 𝑥 ) ↑ 2 ) )
20 19 13 breqtrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
21 4 5 cphsqrtcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( ( 𝑥 , 𝑥 ) ∈ 𝐾 ∧ ( 𝑥 , 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 , 𝑥 ) ) ) → ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ 𝐾 )
22 7 12 18 20 21 syl13anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑥 ∈ 𝑉 ) → ( √ ‘ ( 𝑥 , 𝑥 ) ) ∈ 𝐾 )
23 6 22 fmpt3d ⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 : 𝑉 ⟶ 𝐾 )