Theorem lmodvscl 20875

Description: Closure of scalar product for a left module. (hvmulcl 31109 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 262	. 2 ⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2		pm4.24 568	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 568	. 2 ⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4		lmodvscl.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2740	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2740	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2740	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2740	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20862	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 495	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1148	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1167	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  1_rcur 20160  LModclmod 20857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-lmod 20859

This theorem is referenced by:  lmodvscld  20876  lmodscaf  20881  lmod0vs  20892  lmodvsmmulgdi  20894  lcomf  20898  lmodvneg1  20902  lmodvsneg  20903  lmodnegadd  20908  lmodsubvs  20915  lmodsubdi  20916  lmodsubdir  20917  lmodvsghm  20920  lmodprop2d  20921  lss1  20935  lssvsubcl  20941  lssvscl  20952  lss1d  20960  lssacs  20964  prdsvscacl  20965  lmodvsinv  21033  lmodvsinv2  21034  islmhm2  21035  0lmhm  21037  idlmhm  21038  lmhmco  21040  lmhmplusg  21041  lmhmvsca  21042  lmhmf1o  21043  lmhmpreima  21045  lmhmeql  21052  pwsdiaglmhm  21054  pwssplit3  21058  lvecvscan  21111  lvecvscan2  21112  lspsnvs  21114  lspfixed  21128  lspexch  21129  lspsolvlem  21142  lspsolv  21143  islbs2  21154  ipass  21627  ipassr  21628  phlssphl  21641  ocvlss  21654  dsmmlss  21726  frlmvscavalb  21752  frlmvplusgscavalb  21753  frlmphl  21763  uvcresum  21775  frlmssuvc2  21777  frlmup1  21780  lindfmm  21809  islindf4  21820  assa2ass  21845  assapropd  21853  asclf  21863  assamulgscmlem1  21881  assamulgscmlem2  21882  mplcoe1  22020  mplmon2cl  22051  mplmon2mul  22052  mplind  22053  ply1tmcl  22265  ply1coe  22291  evl1gsummon  22358  evls1fpws  22362  evls1vsca  22366  asclply1subcl  22367  evls1maplmhm  22370  matvscl  22421  mat0dimscm  22459  matinv  22667  mply1topmatcl  22795  pm2mpmhmlem2  22809  monmat2matmon  22814  chpmat1dlem  22825  chpmat1d  22826  chpdmatlem0  22827  chfacfscmulcl  22847  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  cpmadugsumfi  22867  cpmidgsum2  22869  nlmdsdi  24671  nlmdsdir  24672  nlmmul0or  24673  nlmvscnlem2  24675  nlmvscn  24677  clmvscl  25080  cmodscmulexp  25114  cph2ass  25205  ipcau2  25226  tcphcphlem2  25228  tcphcph  25229  cphipval2  25233  4cphipval2  25234  cphipval  25235  pjthlem1  25429  mdegvscale  26065  mdegvsca  26066  plypf1  26202  ttgcontlem1  28978  lmodvslmhm  33138  eqgvscpbl  33440  qusvscpbl  33441  qusvsval  33442  imaslmod  33443  linds2eq  33471  lmhmqusker  33507  ply1degltlss  33686  gsummoncoe1fzo  33687  tngdim  33804  matdim  33806  lindsunlem  33815  lbsdiflsp0  33817  fedgmullem1  33820  fedgmullem2  33821  sitgclbn  34534  lindsadd  37987  lindsenlbs  37989  lfl0  39564  lflsub  39566  lflmul  39567  lfl0f  39568  lfl1  39569  lfladdcl  39570  lflnegcl  39574  lflvscl  39576  lkrlss  39594  eqlkr  39598  lkrlsp  39601  lshpkrlem4  39612  lshpkrlem5  39613  lshpkrlem6  39614  lclkrlem2m  42018  lclkrlem2p  42021  lcdvscl  42104  baerlem3lem1  42206  baerlem5alem1  42207  baerlem5blem1  42208  hdmap14lem1a  42365  hdmap14lem2a  42366  hdmap14lem2N  42368  hdmap14lem3  42369  hdmap14lem4a  42370  hdmap14lem8  42374  hgmapadd  42393  hgmapmul  42394  hgmaprnlem4N  42398  hgmap11  42401  hdmapgln2  42411  hdmapinvlem3  42419  hdmapinvlem4  42420  hdmapglem7b  42427  hlhilphllem  42458  mendassa  43642  ply1mulgsum  48888  lincfsuppcl  48911  linccl  48912  lincvalsng  48914  lincvalpr  48916  lincdifsn  48922  linc1  48923  lincsum  48927  lincscm  48928  lincscmcl  48930  lincext3  48954  lindslinindimp2lem4  48959  lindslinindsimp2  48961  snlindsntor  48969  lincresunit3lem2  48978  lincresunit3  48979  zlmodzxzldeplem3  49000