Metamath Proof Explorer


Theorem cvsclm

Description: A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019)

Ref Expression
Hypothesis cvslvec.1
|- ( ph -> W e. CVec )
Assertion cvsclm
|- ( ph -> W e. CMod )

Proof

Step Hyp Ref Expression
1 cvslvec.1
 |-  ( ph -> W e. CVec )
2 df-cvs
 |-  CVec = ( CMod i^i LVec )
3 2 elin2
 |-  ( W e. CVec <-> ( W e. CMod /\ W e. LVec ) )
4 3 simplbi
 |-  ( W e. CVec -> W e. CMod )
5 1 4 syl
 |-  ( ph -> W e. CMod )