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