Theorem lmodvscl 20799

Description: Closure of scalar product for a left module. (hvmulcl 30975 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypotheses

Ref	Expression
lmodvscl.v	⊢ 𝑉 = (Base‘𝑊)
lmodvscl.f	⊢ 𝐹 = (Scalar‘𝑊)
lmodvscl.s	⊢ · = ( ·𝑠 ‘𝑊)
lmodvscl.k	⊢ 𝐾 = (Base‘𝐹)

Assertion

Ref	Expression
lmodvscl	⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Proof of Theorem lmodvscl

Step	Hyp	Ref	Expression
1		biid 261	. 2 ⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2		pm4.24 563	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 563	. 2 ⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4		lmodvscl.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2729	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2729	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2729	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2729	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20786	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 494	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1142	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1161	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  Scalarcsca 17182   ·_𝑠 cvsca 17183  1_rcur 20084  LModclmod 20781

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-lmod 20783

This theorem is referenced by:  lmodvscld  20800  lmodscaf  20805  lmod0vs  20816  lmodvsmmulgdi  20818  lcomf  20822  lmodvneg1  20826  lmodvsneg  20827  lmodnegadd  20832  lmodsubvs  20839  lmodsubdi  20840  lmodsubdir  20841  lmodvsghm  20844  lmodprop2d  20845  lss1  20859  lssvsubcl  20865  lssvscl  20876  lss1d  20884  lssacs  20888  prdsvscacl  20889  lmodvsinv  20958  lmodvsinv2  20959  islmhm2  20960  0lmhm  20962  idlmhm  20963  lmhmco  20965  lmhmplusg  20966  lmhmvsca  20967  lmhmf1o  20968  lmhmpreima  20970  lmhmeql  20977  pwsdiaglmhm  20979  pwssplit3  20983  lvecvscan  21036  lvecvscan2  21037  lspsnvs  21039  lspfixed  21053  lspexch  21054  lspsolvlem  21067  lspsolv  21068  islbs2  21079  ipass  21570  ipassr  21571  phlssphl  21584  ocvlss  21597  dsmmlss  21669  frlmvscavalb  21695  frlmvplusgscavalb  21696  frlmphl  21706  uvcresum  21718  frlmssuvc2  21720  frlmup1  21723  lindfmm  21752  islindf4  21763  assa2ass  21788  assapropd  21797  asclf  21807  assamulgscmlem1  21824  assamulgscmlem2  21825  mplcoe1  21960  mplmon2cl  21991  mplmon2mul  21992  mplind  21993  ply1tmcl  22174  ply1coe  22201  evl1gsummon  22268  evls1fpws  22272  evls1vsca  22276  asclply1subcl  22277  evls1maplmhm  22280  matvscl  22334  mat0dimscm  22372  matinv  22580  mply1topmatcl  22708  pm2mpmhmlem2  22722  monmat2matmon  22727  chpmat1dlem  22738  chpmat1d  22739  chpdmatlem0  22740  chfacfscmulcl  22760  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cpmadugsumfi  22780  cpmidgsum2  22782  nlmdsdi  24585  nlmdsdir  24586  nlmmul0or  24587  nlmvscnlem2  24589  nlmvscn  24591  clmvscl  25004  cmodscmulexp  25038  cph2ass  25129  ipcau2  25150  tcphcphlem2  25152  tcphcph  25153  cphipval2  25157  4cphipval2  25158  cphipval  25159  pjthlem1  25353  mdegvscale  25996  mdegvsca  25997  plypf1  26133  ttgcontlem1  28848  lmodvslmhm  33016  eqgvscpbl  33297  qusvscpbl  33298  qusvsval  33299  imaslmod  33300  linds2eq  33328  lmhmqusker  33364  ply1degltlss  33538  gsummoncoe1fzo  33539  tngdim  33585  matdim  33587  lindsunlem  33596  lbsdiflsp0  33598  fedgmullem1  33601  fedgmullem2  33602  sitgclbn  34310  lindsadd  37592  lindsenlbs  37594  lfl0  39043  lflsub  39045  lflmul  39046  lfl0f  39047  lfl1  39048  lfladdcl  39049  lflnegcl  39053  lflvscl  39055  lkrlss  39073  eqlkr  39077  lkrlsp  39080  lshpkrlem4  39091  lshpkrlem5  39092  lshpkrlem6  39093  lclkrlem2m  41498  lclkrlem2p  41501  lcdvscl  41584  baerlem3lem1  41686  baerlem5alem1  41687  baerlem5blem1  41688  hdmap14lem1a  41845  hdmap14lem2a  41846  hdmap14lem2N  41848  hdmap14lem3  41849  hdmap14lem4a  41850  hdmap14lem8  41854  hgmapadd  41873  hgmapmul  41874  hgmaprnlem4N  41878  hgmap11  41881  hdmapgln2  41891  hdmapinvlem3  41899  hdmapinvlem4  41900  hdmapglem7b  41907  hlhilphllem  41938  mendassa  43163  ply1mulgsum  48376  lincfsuppcl  48399  linccl  48400  lincvalsng  48402  lincvalpr  48404  lincdifsn  48410  linc1  48411  lincsum  48415  lincscm  48416  lincscmcl  48418  lincext3  48442  lindslinindimp2lem4  48447  lindslinindsimp2  48449  snlindsntor  48457  lincresunit3lem2  48466  lincresunit3  48467  zlmodzxzldeplem3  48488