Theorem clmlmod 24814

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  (class class class)co 7411  Basecbs 17148   ↾_s cress 17177  Scalarcsca 17204  SubRingcsubrg 20457  LModclmod 20614  ℂ_fldccnfld 21144  ℂModcclm 24809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-clm 24810

This theorem is referenced by:  clmgrp  24815  clmabl  24816  clmring  24817  clmfgrp  24818  clmvscl  24835  clmvsass  24836  clmvsdir  24838  clmvsdi  24839  clmvs1  24840  clmvs2  24841  clm0vs  24842  clmopfne  24843  clmvneg1  24846  clmvsneg  24847  clmsubdir  24849  clmvsubval  24856  zlmclm  24859  cmodscmulexp  24869  iscvs  24874  cvsi  24877  isncvsngp  24897  ttgbtwnid  28408  ttgcontlem1  28409