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	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )

Proof

Step	Hyp	Ref	Expression
1		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
2	1	elin2	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) )
3		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
4		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5	4	islvec	⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )
6	5	a1i	⊢ ( 𝑊 ∈ ℂMod → ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) ) )
7	3 6	mpbirand	⊢ ( 𝑊 ∈ ℂMod → ( 𝑊 ∈ LVec ↔ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )
8	7	pm5.32i	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec ) ↔ ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )
9	2 8	bitri	⊢ ( 𝑊 ∈ ℂVec ↔ ( 𝑊 ∈ ℂMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )