This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ ℂ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 ) )