Theorem lmodvscl 20829

Description: Closure of scalar product for a left module. (hvmulcl 31088 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 2736	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2736	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2736	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2736	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20816	. . . 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 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Scalarcsca 17180   ·_𝑠 cvsca 17181  1_rcur 20116  LModclmod 20811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-lmod 20813

This theorem is referenced by:  lmodvscld  20830  lmodscaf  20835  lmod0vs  20846  lmodvsmmulgdi  20848  lcomf  20852  lmodvneg1  20856  lmodvsneg  20857  lmodnegadd  20862  lmodsubvs  20869  lmodsubdi  20870  lmodsubdir  20871  lmodvsghm  20874  lmodprop2d  20875  lss1  20889  lssvsubcl  20895  lssvscl  20906  lss1d  20914  lssacs  20918  prdsvscacl  20919  lmodvsinv  20988  lmodvsinv2  20989  islmhm2  20990  0lmhm  20992  idlmhm  20993  lmhmco  20995  lmhmplusg  20996  lmhmvsca  20997  lmhmf1o  20998  lmhmpreima  21000  lmhmeql  21007  pwsdiaglmhm  21009  pwssplit3  21013  lvecvscan  21066  lvecvscan2  21067  lspsnvs  21069  lspfixed  21083  lspexch  21084  lspsolvlem  21097  lspsolv  21098  islbs2  21109  ipass  21600  ipassr  21601  phlssphl  21614  ocvlss  21627  dsmmlss  21699  frlmvscavalb  21725  frlmvplusgscavalb  21726  frlmphl  21736  uvcresum  21748  frlmssuvc2  21750  frlmup1  21753  lindfmm  21782  islindf4  21793  assa2ass  21818  assapropd  21827  asclf  21837  assamulgscmlem1  21855  assamulgscmlem2  21856  mplcoe1  21992  mplmon2cl  22023  mplmon2mul  22024  mplind  22025  ply1tmcl  22214  ply1coe  22242  evl1gsummon  22309  evls1fpws  22313  evls1vsca  22317  asclply1subcl  22318  evls1maplmhm  22321  matvscl  22375  mat0dimscm  22413  matinv  22621  mply1topmatcl  22749  pm2mpmhmlem2  22763  monmat2matmon  22768  chpmat1dlem  22779  chpmat1d  22780  chpdmatlem0  22781  chfacfscmulcl  22801  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmidgsum2  22823  nlmdsdi  24625  nlmdsdir  24626  nlmmul0or  24627  nlmvscnlem2  24629  nlmvscn  24631  clmvscl  25044  cmodscmulexp  25078  cph2ass  25169  ipcau2  25190  tcphcphlem2  25192  tcphcph  25193  cphipval2  25197  4cphipval2  25198  cphipval  25199  pjthlem1  25393  mdegvscale  26036  mdegvsca  26037  plypf1  26173  ttgcontlem1  28957  lmodvslmhm  33133  eqgvscpbl  33431  qusvscpbl  33432  qusvsval  33433  imaslmod  33434  linds2eq  33462  lmhmqusker  33498  ply1degltlss  33677  gsummoncoe1fzo  33678  tngdim  33770  matdim  33772  lindsunlem  33781  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  sitgclbn  34500  lindsadd  37810  lindsenlbs  37812  lfl0  39321  lflsub  39323  lflmul  39324  lfl0f  39325  lfl1  39326  lfladdcl  39327  lflnegcl  39331  lflvscl  39333  lkrlss  39351  eqlkr  39355  lkrlsp  39358  lshpkrlem4  39369  lshpkrlem5  39370  lshpkrlem6  39371  lclkrlem2m  41775  lclkrlem2p  41778  lcdvscl  41861  baerlem3lem1  41963  baerlem5alem1  41964  baerlem5blem1  41965  hdmap14lem1a  42122  hdmap14lem2a  42123  hdmap14lem2N  42125  hdmap14lem3  42126  hdmap14lem4a  42127  hdmap14lem8  42131  hgmapadd  42150  hgmapmul  42151  hgmaprnlem4N  42155  hgmap11  42158  hdmapgln2  42168  hdmapinvlem3  42176  hdmapinvlem4  42177  hdmapglem7b  42184  hlhilphllem  42215  mendassa  43428  ply1mulgsum  48632  lincfsuppcl  48655  linccl  48656  lincvalsng  48658  lincvalpr  48660  lincdifsn  48666  linc1  48667  lincsum  48671  lincscm  48672  lincscmcl  48674  lincext3  48698  lindslinindimp2lem4  48703  lindslinindsimp2  48705  snlindsntor  48713  lincresunit3lem2  48722  lincresunit3  48723  zlmodzxzldeplem3  48744