Theorem cphreccl

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

	Ref	Expression
Hypotheses	cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	cphsca.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphreccl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\wedge A\ne 0\right)\to \frac{1}{A}\in K$$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		cphsca.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	cphsca	$$⊢W\in \mathrm{CPreHil}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
4		cphlvec	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LVec}$$
5	1	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
6	4 5	syl	$$⊢W\in \mathrm{CPreHil}\to F\in \mathrm{DivRing}$$
7	2 3 6	cphreccllem	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in K\wedge A\ne 0\right)\to \frac{1}{A}\in K$$