Theorem lmodvscl 20898

Description: Closure of scalar product for a left module. (hvmulcl 31045 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 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 20885	. . . 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 1087   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  1_rcur 20208  LModclmod 20880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-lmod 20882

This theorem is referenced by:  lmodvscld  20899  lmodscaf  20904  lmod0vs  20915  lmodvsmmulgdi  20917  lcomf  20921  lmodvneg1  20925  lmodvsneg  20926  lmodnegadd  20931  lmodsubvs  20938  lmodsubdi  20939  lmodsubdir  20940  lmodvsghm  20943  lmodprop2d  20944  lss1  20959  lssvsubcl  20965  lssvscl  20976  lss1d  20984  lssacs  20988  prdsvscacl  20989  lmodvsinv  21058  lmodvsinv2  21059  islmhm2  21060  0lmhm  21062  idlmhm  21063  lmhmco  21065  lmhmplusg  21066  lmhmvsca  21067  lmhmf1o  21068  lmhmpreima  21070  lmhmeql  21077  pwsdiaglmhm  21079  pwssplit3  21083  lvecvscan  21136  lvecvscan2  21137  lspsnvs  21139  lspfixed  21153  lspexch  21154  lspsolvlem  21167  lspsolv  21168  islbs2  21179  ipass  21686  ipassr  21687  phlssphl  21700  ocvlss  21713  dsmmlss  21787  frlmvscavalb  21813  frlmvplusgscavalb  21814  frlmphl  21824  uvcresum  21836  frlmssuvc2  21838  frlmup1  21841  lindfmm  21870  islindf4  21881  assa2ass  21906  assapropd  21915  asclf  21925  assamulgscmlem1  21942  assamulgscmlem2  21943  mplcoe1  22078  mplmon2cl  22115  mplmon2mul  22116  mplind  22117  ply1tmcl  22296  ply1coe  22323  evl1gsummon  22390  evls1fpws  22394  evls1vsca  22398  asclply1subcl  22399  evls1maplmhm  22402  matvscl  22458  mat0dimscm  22496  matinv  22704  mply1topmatcl  22832  pm2mpmhmlem2  22846  monmat2matmon  22851  chpmat1dlem  22862  chpmat1d  22863  chpdmatlem0  22864  chfacfscmulcl  22884  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmidgsum2  22906  nlmdsdi  24723  nlmdsdir  24724  nlmmul0or  24725  nlmvscnlem2  24727  nlmvscn  24729  clmvscl  25140  cmodscmulexp  25174  cph2ass  25266  ipcau2  25287  tcphcphlem2  25289  tcphcph  25290  cphipval2  25294  4cphipval2  25295  cphipval  25296  pjthlem1  25490  mdegvscale  26134  mdegvsca  26135  plypf1  26271  ttgcontlem1  28917  lmodvslmhm  33033  eqgvscpbl  33343  qusvscpbl  33344  qusvsval  33345  imaslmod  33346  linds2eq  33374  lmhmqusker  33410  ply1degltlss  33582  gsummoncoe1fzo  33583  tngdim  33626  matdim  33628  lindsunlem  33637  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  sitgclbn  34308  lindsadd  37573  lindsenlbs  37575  lfl0  39021  lflsub  39023  lflmul  39024  lfl0f  39025  lfl1  39026  lfladdcl  39027  lflnegcl  39031  lflvscl  39033  lkrlss  39051  eqlkr  39055  lkrlsp  39058  lshpkrlem4  39069  lshpkrlem5  39070  lshpkrlem6  39071  lclkrlem2m  41476  lclkrlem2p  41479  lcdvscl  41562  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  hdmap14lem1a  41823  hdmap14lem2a  41824  hdmap14lem2N  41826  hdmap14lem3  41827  hdmap14lem4a  41828  hdmap14lem8  41832  hgmapadd  41851  hgmapmul  41852  hgmaprnlem4N  41856  hgmap11  41859  hdmapgln2  41869  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem7b  41885  hlhilphllem  41920  mendassa  43151  ply1mulgsum  48119  lincfsuppcl  48142  linccl  48143  lincvalsng  48145  lincvalpr  48147  lincdifsn  48153  linc1  48154  lincsum  48158  lincscm  48159  lincscmcl  48161  lincext3  48185  lindslinindimp2lem4  48190  lindslinindsimp2  48192  snlindsntor  48200  lincresunit3lem2  48209  lincresunit3  48210  zlmodzxzldeplem3  48231