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