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 
|- ( W e. CPreHil -> W e. CMod )

Proof

Step Hyp Ref Expression
1 cphlmod 
 |-  ( W e. CPreHil -> W e. LMod )
2 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
3 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
4 2 3 cphsca 
 |-  ( W e. CPreHil -> ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) )
5 2 3 cphsubrg 
 |-  ( W e. CPreHil -> ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) )
6 2 3 isclm 
 |-  ( W e. CMod <-> ( W e. LMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) /\ ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) ) )
7 1 4 5 6 syl3anbrc 
 |-  ( W e. CPreHil -> W e. CMod )