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 = ( Scalar ` W )
	cphsca.k	|- K = ( Base ` F )
Assertion	cphreccl	|- ( ( W e. CPreHil /\ A e. K /\ A =/= 0 ) -> ( 1 / A ) e. K )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	|- F = ( Scalar ` W )
2		cphsca.k	|- K = ( Base ` F )
3	1 2	cphsca	|- ( W e. CPreHil -> F = ( CCfld |`s K ) )
4		cphlvec	|- ( W e. CPreHil -> W e. LVec )
5	1	lvecdrng	|- ( W e. LVec -> F e. DivRing )
6	4 5	syl	|- ( W e. CPreHil -> F e. DivRing )
7	2 3 6	cphreccllem	|- ( ( W e. CPreHil /\ A e. K /\ A =/= 0 ) -> ( 1 / A ) e. K )