Theorem clmlmod 24467

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 2731	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2		eqid 2731	. . 3 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
3	1, 2	isclm 24464	. 2 ⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) = (ℂfld ↾s (Base‘(Scalar‘𝑊))) ∧ (Base‘(Scalar‘𝑊)) ∈ (SubRing‘ℂfld)))
4	3	simp1bi 1145	1 ⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  Basecbs 17094   ↾_s cress 17123  Scalarcsca 17150  SubRingcsubrg 20266  LModclmod 20378  ℂ_fldccnfld 20833  ℂModcclm 24462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-clm 24463

This theorem is referenced by:  clmgrp  24468  clmabl  24469  clmring  24470  clmfgrp  24471  clmvscl  24488  clmvsass  24489  clmvsdir  24491  clmvsdi  24492  clmvs1  24493  clmvs2  24494  clm0vs  24495  clmopfne  24496  clmvneg1  24499  clmvsneg  24500  clmsubdir  24502  clmvsubval  24509  zlmclm  24512  cmodscmulexp  24522  iscvs  24527  cvsi  24530  isncvsngp  24550  ttgbtwnid  27895  ttgcontlem1  27896