Theorem lveclmod 21238

Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013.)

Assertion

Ref	Expression
lveclmod	⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

Proof of Theorem lveclmod

Step	Hyp	Ref	Expression
1		eqid 2762	. . 3 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
2	1	islvec 21236	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ DivRing))
3	2	simplbi 501	1 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ‘cfv 6536  Scalarcsca 17319  DivRingcdr 20838  LModclmod 20992  LVecclvec 21234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-lvec 21235

This theorem is used by:  lveclmodd  21239  lsslvec  21241  lvecvs0or  21243  lssvs0or  21245  lvecvscan  21246  lvecvscan2  21247  lvecinv  21248  lspsnvs  21249  lspsneleq  21250  lspsncmp  21251  lspsnne1  21252  lspsnnecom  21254  lspabs2  21255  lspabs3  21256  lspsneq  21257  ellspsn4  21259  lspdisj  21260  lspdisjb  21261  lspdisj2  21262  lspfixed  21263  lspexch  21264  lspexchn1  21265  lspindpi  21267  lvecindp  21273  lvecindp2  21274  lsmcv  21276  lspsolv  21278  lssacsex  21279  lspsnat  21280  lsppratlem2  21283  lsppratlem3  21284  lsppratlem4  21285  lsppratlem6  21287  lspprat  21288  islbs2  21289  islbs3  21290  lbsacsbs  21291  lbsextlem2  21294  lbsextlem3  21295  lbsextlem4  21296  phllmod  21791  isphld  21815  islinds4  21996  lvecisfrlm  22004  cvsi  25300  0nellinds  33694  lindssn  33700  linds2eq  33703  exsslsb  33996  lvecdim0i  34005  lssdimle  34007  tngdim  34012  matdim  34014  lbslsat  34015  lsatdim  34016  drngdimgt0  34017  lindsunlem  34023  lindsun  34024  lbsdiflsp0  34025  dimkerim  34026  qusdimsum  34027  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  extdg1id  34065  ccfldextdgrr  34071  lindsadd  38292  lshpnelb  39786  lshpnel2N  39787  lshpdisj  39789  lshpcmp  39790  lsatcmp  39805  lsatcmp2  39806  lsatel  39807  lsatelbN  39808  lsatfixedN  39811  lsmcv2  39831  lsatcv0  39833  lsatcveq0  39834  lsat0cv  39835  lcvp  39842  lcv1  39843  lcv2  39844  lsatexch  39845  lsatnem0  39847  lsatexch1  39848  lsatcv0eq  39849  lsatcv1  39850  lsatcvatlem  39851  lsatcvat  39852  lsatcvat2  39853  lsatcvat3  39854  islshpcv  39855  l1cvpat  39856  l1cvat  39857  lfl1  39872  lkrsc  39899  lkrscss  39900  eqlkr  39901  eqlkr3  39903  lkrlsp  39904  lkrlsp3  39906  lkrshp  39907  lkrshp3  39908  lkrshpor  39909  lkrshp4  39910  lshpsmreu  39911  lshpkrlem1  39912  lshpkrlem4  39915  lshpkrlem5  39916  lshpkrlem6  39917  lshpkr  39919  lshpkrex  39920  lfl1dim  39923  lfl1dim2N  39924  lduallvec  39956  lduallkr3  39964  lkrpssN  39965  ldual1dim  39968  lkrss2N  39971  lkreqN  39972  lkrlspeqN  39973  dva0g  41829  dia1dim2  41864  dia1dimid  41865  dia2dimlem5  41870  dia2dimlem7  41872  dia2dimlem9  41874  dia2dimlem10  41875  dia2dimlem13  41878  dvhlmod  41912  diblsmopel  41973  lclkrlem2m  42321  lclkrlem2n  42322  lcfrlem1  42344  lcfrlem2  42345  lcfrlem3  42346  lcdlmod  42394  baerlem3lem1  42509  baerlem5alem1  42510  baerlem5blem1  42511  baerlem3lem2  42512  baerlem5alem2  42513  baerlem5blem2  42514  baerlem5amN  42518  baerlem5bmN  42519  baerlem5abmN  42520  mapdindp0  42521  mapdindp1  42522  mapdindp2  42523  mapdindp3  42524  mapdindp4  42525  lspindp5  42572  lvecgrp  43333  lvecring  43334  prjspersym  43367  prjsper  43368  prjspreln0  43369  prjspvs  43370  prjspeclsp  43372  0prjspn  43388  lincreslvec3  49290  isldepslvec2  49293  lindssnlvec  49294  lvecpsslmod  49315