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 ⊢ F = Scalar ⁡ W
cphsca.k ⊢ K = Base F
Assertion cphsca ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ F = Scalar ⁡ W
2 cphsca.k ⊢ K = Base F
3 eqid ⊢ Base W = Base W
4 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
5 eqid ⊢ norm ⁡ W = norm ⁡ W
6 3 4 5 1 2 iscph ⊢ W ∈ CPreHil ↔ W ∈ PreHil ∧ W ∈ NrmMod ∧ F = ℂ fld ↾ 𝑠 K ∧ √ K ∩ 0 +∞ ⊆ K ∧ norm ⁡ W = x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x
7 6 simp1bi ⊢ W ∈ CPreHil → W ∈ PreHil ∧ W ∈ NrmMod ∧ F = ℂ fld ↾ 𝑠 K
8 7 simp3d ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K