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 = Scalar (W)$
	cphsca.k	$⊢ K = {Base}_{F}$
Assertion	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$

Step	Hyp	Ref	Expression
1		cphsca.f	$⊢ F = Scalar (W)$
2		cphsca.k	$⊢ K = {Base}_{F}$
3	1 2	cphsca	$⊢ W \in CPreHil \to F = ℂ_{fld} ↾_{𝑠} K$
4		cphlvec	$⊢ W \in CPreHil \to W \in LVec$
5	1	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
6	4 5	syl	$⊢ W \in CPreHil \to F \in DivRing$
7	2 3 6	cphsubrglem	$⊢ W \in CPreHil \to (F = ℂ_{fld} ↾_{𝑠} K \land K = K \cap ℂ \land K \in SubRing (ℂ_{fld}))$
8	7	simp3d	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$

Metamath Proof Explorer