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 β†’ 𝑁 : 𝑉 ⟢ 𝐾 )