Theorem cvsclm

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

	Ref	Expression
Hypothesis	cvslvec.1	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
Assertion	cvsclm	⊢ ( 𝜑 → 𝑊 ∈ ℂMod )

Proof

Step	Hyp	Ref	Expression
1		cvslvec.1	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
2		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
3	2	elin2	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) )
4	3	simplbi	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
5	1 4	syl	⊢ ( 𝜑 → 𝑊 ∈ ℂMod )