Metamath Proof Explorer


Theorem cphsubrg

Description: The scalar field of a subcomplex pre-Hilbert space is a subring of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsca.f F=ScalarW
cphsca.k K=BaseF
Assertion cphsubrg WCPreHilKSubRingfld

Proof

Step Hyp Ref Expression
1 cphsca.f F=ScalarW
2 cphsca.k K=BaseF
3 1 2 cphsca WCPreHilF=fld𝑠K
4 cphlvec WCPreHilWLVec
5 1 lvecdrng WLVecFDivRing
6 4 5 syl WCPreHilFDivRing
7 2 3 6 cphsubrglem WCPreHilF=fld𝑠KK=KKSubRingfld
8 7 simp3d WCPreHilKSubRingfld