Theorem clmlmod 24983

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

Assertion

Ref	Expression
clmlmod	⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod)

Proof of Theorem clmlmod

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2		eqid 2729	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3	1, 2	isclm 24980	. 2 ⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))) ∧ (Base‘(Scalar‘𝑊)) ∈ (SubRing‘ℂfld)))
4	3	simp1bi 1145	1 ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138   ↾_s cress 17159  Scalarcsca 17182  SubRingcsubrg 20472  LModclmod 20781  ℂ_fldccnfld 21279  ℂModcclm 24978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-clm 24979

This theorem is referenced by:  clmgrp  24984  clmabl  24985  clmring  24986  clmfgrp  24987  clmvscl  25004  clmvsass  25005  clmvsdir  25007  clmvsdi  25008  clmvs1  25009  clmvs2  25010  clm0vs  25011  clmopfne  25012  clmvneg1  25015  clmvsneg  25016  clmsubdir  25018  clmvsubval  25025  zlmclm  25028  cmodscmulexp  25038  iscvs  25043  cvsi  25046  isncvsngp  25065  ttgbtwnid  28847  ttgcontlem1  28848