Metamath Proof Explorer

Theorem cphclm

Description: A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion cphclm ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ β„‚Mod )

Proof

Step Hyp Ref Expression
1 cphlmod ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ LMod )
2 eqid ⊒ ( Scalar β€˜ π‘Š ) = ( Scalar β€˜ π‘Š )
3 eqid ⊒ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) = ( Base β€˜ ( Scalar β€˜ π‘Š ) )
4 2 3 cphsca ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( Scalar β€˜ π‘Š ) = ( β„‚fld β†Ύs ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ) )
5 2 3 cphsubrg ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∈ ( SubRing β€˜ β„‚fld ) )
6 2 3 isclm ⊒ ( π‘Š ∈ β„‚Mod ↔ ( π‘Š ∈ LMod ∧ ( Scalar β€˜ π‘Š ) = ( β„‚fld β†Ύs ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ) ∧ ( Base β€˜ ( Scalar β€˜ π‘Š ) ) ∈ ( SubRing β€˜ β„‚fld ) ) )
7 1 4 5 6 syl3anbrc ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ β„‚Mod )