Theorem lmodvscl 20716

Description: Closure of scalar product for a left module. (hvmulcl 30738 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 2724	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2724	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2724	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2724	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20703	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 494	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1139	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1158	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ‘cfv 6534  (class class class)co 7402  Basecbs 17145  +_gcplusg 17198  ._rcmulr 17199  Scalarcsca 17201   ·_𝑠 cvsca 17202  1_rcur 20078  LModclmod 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5297

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rab 3425  df-v 3468  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405  df-lmod 20700

This theorem is referenced by:  lmodvscld  20717  lmodscaf  20722  lmod0vs  20733  lmodvsmmulgdi  20735  lcomf  20739  lmodvneg1  20743  lmodvsneg  20744  lmodnegadd  20749  lmodsubvs  20756  lmodsubdi  20757  lmodsubdir  20758  lmodvsghm  20761  lmodprop2d  20762  lss1  20777  lssvsubcl  20783  lssvscl  20794  lss1d  20802  lssacs  20806  prdsvscacl  20807  lmodvsinv  20876  lmodvsinv2  20877  islmhm2  20878  0lmhm  20880  idlmhm  20881  lmhmco  20883  lmhmplusg  20884  lmhmvsca  20885  lmhmf1o  20886  lmhmpreima  20888  lmhmeql  20895  pwsdiaglmhm  20897  pwssplit3  20901  lvecvscan  20954  lvecvscan2  20955  lspsnvs  20957  lspfixed  20971  lspexch  20972  lspsolvlem  20985  lspsolv  20986  islbs2  20997  ipass  21508  ipassr  21509  phlssphl  21522  ocvlss  21535  dsmmlss  21609  frlmvscavalb  21635  frlmvplusgscavalb  21636  frlmphl  21646  uvcresum  21658  frlmssuvc2  21660  frlmup1  21663  lindfmm  21692  islindf4  21703  assa2ass  21728  assapropd  21736  asclf  21746  assamulgscmlem1  21763  assamulgscmlem2  21764  mplcoe1  21904  mplmon2cl  21941  mplmon2mul  21942  mplind  21943  mhpvscacl  22007  ply1tmcl  22115  ply1coe  22141  evl1gsummon  22208  matvscl  22257  mat0dimscm  22295  matinv  22503  mply1topmatcl  22631  pm2mpmhmlem2  22645  monmat2matmon  22650  chpmat1dlem  22661  chpmat1d  22662  chpdmatlem0  22663  chfacfscmulcl  22683  cpmadugsumlemB  22700  cpmadugsumlemC  22701  cpmadugsumlemF  22702  cpmadugsumfi  22703  cpmidgsum2  22705  nlmdsdi  24522  nlmdsdir  24523  nlmmul0or  24524  nlmvscnlem2  24526  nlmvscn  24528  clmvscl  24939  cmodscmulexp  24973  cph2ass  25065  ipcau2  25086  tcphcphlem2  25088  tcphcph  25089  cphipval2  25093  4cphipval2  25094  cphipval  25095  pjthlem1  25289  mdegvscale  25935  mdegvsca  25936  plypf1  26068  ttgcontlem1  28614  lmodvslmhm  32673  eqgvscpbl  32934  qusvscpbl  32935  qusvsval  32936  imaslmod  32937  linds2eq  32969  lmhmqusker  33006  evls1fpws  33116  evls1vsca  33120  asclply1subcl  33130  ply1degltlss  33136  gsummoncoe1fzo  33137  tngdim  33180  matdim  33182  lindsunlem  33191  lbsdiflsp0  33193  fedgmullem1  33196  fedgmullem2  33197  evls1maplmhm  33243  sitgclbn  33834  lindsadd  36975  lindsenlbs  36977  lfl0  38429  lflsub  38431  lflmul  38432  lfl0f  38433  lfl1  38434  lfladdcl  38435  lflnegcl  38439  lflvscl  38441  lkrlss  38459  eqlkr  38463  lkrlsp  38466  lshpkrlem4  38477  lshpkrlem5  38478  lshpkrlem6  38479  lclkrlem2m  40884  lclkrlem2p  40887  lcdvscl  40970  baerlem3lem1  41072  baerlem5alem1  41073  baerlem5blem1  41074  hdmap14lem1a  41231  hdmap14lem2a  41232  hdmap14lem2N  41234  hdmap14lem3  41235  hdmap14lem4a  41236  hdmap14lem8  41240  hgmapadd  41259  hgmapmul  41260  hgmaprnlem4N  41264  hgmap11  41267  hdmapgln2  41277  hdmapinvlem3  41285  hdmapinvlem4  41286  hdmapglem7b  41293  hlhilphllem  41328  mendassa  42450  ply1mulgsum  47284  lincfsuppcl  47307  linccl  47308  lincvalsng  47310  lincvalpr  47312  lincdifsn  47318  linc1  47319  lincsum  47323  lincscm  47324  lincscmcl  47326  lincext3  47350  lindslinindimp2lem4  47355  lindslinindsimp2  47357  snlindsntor  47365  lincresunit3lem2  47374  lincresunit3  47375  zlmodzxzldeplem3  47396