Theorem clmlmod 25187

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  ‘cfv 6525  (class class class)co 7400  Basecbs 17259   ↾_s cress 17280  Scalarcsca 17303  SubRingcsubrg 20645  LModclmod 20950  ℂ_fldccnfld 21482  ℂModcclm 25182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-clm 25183

This theorem is referenced by:  clmgrp  25188  clmabl  25189  clmring  25190  clmfgrp  25191  clmvscl  25208  clmvsass  25209  clmvsdir  25211  clmvsdi  25212  clmvs1  25213  clmvs2  25214  clm0vs  25215  clmopfne  25216  clmvneg1  25219  clmvsneg  25220  clmsubdir  25222  clmvsubval  25229  zlmclm  25232  cmodscmulexp  25242  iscvs  25247  cvsi  25250  isncvsngp  25269  ttgbtwnid  29142  ttgcontlem1  29143