Theorem clmlmod 24981

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  Basecbs 17171   ↾_s cress 17200  Scalarcsca 17227  SubRingcsubrg 20495  LModclmod 20732  ℂ_fldccnfld 21266  ℂModcclm 24976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-nul 5300

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-clm 24977

This theorem is referenced by:  clmgrp  24982  clmabl  24983  clmring  24984  clmfgrp  24985  clmvscl  25002  clmvsass  25003  clmvsdir  25005  clmvsdi  25006  clmvs1  25007  clmvs2  25008  clm0vs  25009  clmopfne  25010  clmvneg1  25013  clmvsneg  25014  clmsubdir  25016  clmvsubval  25023  zlmclm  25026  cmodscmulexp  25036  iscvs  25041  cvsi  25044  isncvsngp  25064  ttgbtwnid  28681  ttgcontlem1  28682