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∈ℂVec↔W∈CMod∧Scalar⁡W∈DivRing

Proof

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