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

Metamath Proof Explorer

Theorem cphsca

Description: A subcomplex pre-Hilbert space is a vector space over a subfield of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cphsca ( 𝑊 ∈ ℂPreHil → 𝐹 = ( ℂfld ↾s 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cphsca.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
5 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
6 3 4 5 1 2 iscph ⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) ∧ ( √ “ ( 𝐾 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝐾 ∧ ( norm ‘ 𝑊 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ) )
7 6 simp1bi ⊢ ( 𝑊 ∈ ℂPreHil → ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
8 7 simp3d ⊢ ( 𝑊 ∈ ℂPreHil → 𝐹 = ( ℂfld ↾s 𝐾 ) )