Theorem clmlmod 25301

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7417  Basecbs 17307   ↾_s cress 17328  Scalarcsca 17351  SubRingcsubrg 20737  LModclmod 21050  ℂ_fldccnfld 21591  ℂModcclm 25296

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-clm 25297

This theorem is used by:  clmgrp  25302  clmabl  25303  clmring  25304  clmfgrp  25305  clmvscl  25322  clmvsass  25323  clmvsdir  25325  clmvsdi  25326  clmvs1  25327  clmvs2  25328  clm0vs  25329  clmopfne  25330  clmvneg1  25333  clmvsneg  25334  clmsubdir  25336  clmvsubval  25343  zlmclm  25346  cmodscmulexp  25356  iscvs  25361  cvsi  25364  isncvsngp  25383  ttgbtwnid  29348  ttgcontlem1  29349