Metamath Proof Explorer


Theorem cphnlm

Description: A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Assertion cphnlm ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
3 eqid ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
4 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 1 2 3 4 5 iscph ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂflds ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∧ ( √ “ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( norm ‘ 𝑊 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖𝑊 ) 𝑥 ) ) ) ) )
7 6 simp1bi ( 𝑊 ∈ ℂPreHil → ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂflds ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
8 7 simp2d ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )