Metamath Proof Explorer

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 ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
cphsca.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
Assertion cphreccl ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 β‰  0 ) β†’ ( 1 / 𝐴 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
2 cphsca.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
3 1 2 cphsca ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐹 = ( β„‚fld β†Ύs 𝐾 ) )
4 cphlvec ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ LVec )
5 1 lvecdrng ⊒ ( π‘Š ∈ LVec β†’ 𝐹 ∈ DivRing )
6 4 5 syl ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐹 ∈ DivRing )
7 2 3 6 cphreccllem ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 β‰  0 ) β†’ ( 1 / 𝐴 ) ∈ 𝐾 )