hlprlem

	Ref	Expression
Hypotheses	hlress.f	$⊢ F = Scalar (W)$
	hlress.k	$⊢ K = {Base}_{F}$
Assertion	hlprlem	$⊢ W \in ℂHil \to (K \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} K \in DivRing \land ℂ_{fld} ↾_{𝑠} K \in CMetSp)$

Step	Hyp	Ref	Expression
1		hlress.f	$⊢ F = Scalar (W)$
2		hlress.k	$⊢ K = {Base}_{F}$
3		hlcph	$⊢ W \in ℂHil \to W \in CPreHil$
4	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
5	3 4	syl	$⊢ W \in ℂHil \to K \in SubRing (ℂ_{fld})$
6	1 2	cphsca	$⊢ W \in CPreHil \to F = ℂ_{fld} ↾_{𝑠} K$
7	3 6	syl	$⊢ W \in ℂHil \to F = ℂ_{fld} ↾_{𝑠} K$
8		cphlvec	$⊢ W \in CPreHil \to W \in LVec$
9	1	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
10	3 8 9	3syl	$⊢ W \in ℂHil \to F \in DivRing$
11	7 10	eqeltrrd	$⊢ W \in ℂHil \to ℂ_{fld} ↾_{𝑠} K \in DivRing$
12		hlbn	$⊢ W \in ℂHil \to W \in Ban$
13	1	bnsca	$⊢ W \in Ban \to F \in CMetSp$
14	12 13	syl	$⊢ W \in ℂHil \to F \in CMetSp$
15	7 14	eqeltrrd	$⊢ W \in ℂHil \to ℂ_{fld} ↾_{𝑠} K \in CMetSp$
16	5 11 15	3jca	$⊢ W \in ℂHil \to (K \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} K \in DivRing \land ℂ_{fld} ↾_{𝑠} K \in CMetSp)$

Metamath Proof Explorer