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

Metamath Proof Explorer

Theorem clmlmod

Description: A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion clmlmod ⊢ W ∈ CMod → W ∈ LMod

Proof

Step Hyp Ref Expression
1 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
2 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
3 1 2 isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ∧ Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld
4 3 simp1bi ⊢ W ∈ CMod → W ∈ LMod