Theorem clmlmod 25109

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ‘cfv 6517  (class class class)co 7392  Basecbs 17228   ↾_s cress 17249  Scalarcsca 17272  SubRingcsubrg 20598  LModclmod 20907  ℂ_fldccnfld 21404  ℂModcclm 25104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-clm 25105

This theorem is referenced by:  clmgrp  25110  clmabl  25111  clmring  25112  clmfgrp  25113  clmvscl  25130  clmvsass  25131  clmvsdir  25133  clmvsdi  25134  clmvs1  25135  clmvs2  25136  clm0vs  25137  clmopfne  25138  clmvneg1  25141  clmvsneg  25142  clmsubdir  25144  clmvsubval  25151  zlmclm  25154  cmodscmulexp  25164  iscvs  25169  cvsi  25172  isncvsngp  25191  ttgbtwnid  29030  ttgcontlem1  29031