Theorem clmlmod 25119

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258   ↾_s cress 17287  Scalarcsca 17314  SubRingcsubrg 20595  LModclmod 20880  ℂ_fldccnfld 21387  ℂModcclm 25114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-clm 25115

This theorem is referenced by:  clmgrp  25120  clmabl  25121  clmring  25122  clmfgrp  25123  clmvscl  25140  clmvsass  25141  clmvsdir  25143  clmvsdi  25144  clmvs1  25145  clmvs2  25146  clm0vs  25147  clmopfne  25148  clmvneg1  25151  clmvsneg  25152  clmsubdir  25154  clmvsubval  25161  zlmclm  25164  cmodscmulexp  25174  iscvs  25179  cvsi  25182  isncvsngp  25202  ttgbtwnid  28916  ttgcontlem1  28917