Metamath Proof Explorer

Theorem iscvs

Description: A subcomplex vector space is a subcomplex module over a division ring. For example, the subcomplex modules over the rational or real or complex numbers are subcomplex vector spaces. (Contributed by AV, 4-Oct-2021)

Ref Expression
Assertion iscvs 
|- ( W e. CVec <-> ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) )

Proof

Step Hyp Ref Expression
1 df-cvs 
 |-  CVec = ( CMod i^i LVec )
2 1 elin2 
 |-  ( W e. CVec <-> ( W e. CMod /\ W e. LVec ) )
3 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
4 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
5 4 islvec 
 |-  ( W e. LVec <-> ( W e. LMod /\ ( Scalar ` W ) e. DivRing ) )
6 5 a1i 
 |-  ( W e. CMod -> ( W e. LVec <-> ( W e. LMod /\ ( Scalar ` W ) e. DivRing ) ) )
7 3 6 mpbirand 
 |-  ( W e. CMod -> ( W e. LVec <-> ( Scalar ` W ) e. DivRing ) )
8 7 pm5.32i 
 |-  ( ( W e. CMod /\ W e. LVec ) <-> ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) )
9 2 8 bitri 
 |-  ( W e. CVec <-> ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) )