Theorem lmodvscl 20831

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  (class class class)co 7358  Basecbs 17137  +_gcplusg 17178  ._rcmulr 17179  Scalarcsca 17181   ·_𝑠 cvsca 17182  1_rcur 20120  LModclmod 20813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-lmod 20815

This theorem is referenced by:  lmodvscld  20832  lmodscaf  20837  lmod0vs  20848  lmodvsmmulgdi  20850  lcomf  20854  lmodvneg1  20858  lmodvsneg  20859  lmodnegadd  20864  lmodsubvs  20871  lmodsubdi  20872  lmodsubdir  20873  lmodvsghm  20876  lmodprop2d  20877  lss1  20891  lssvsubcl  20897  lssvscl  20908  lss1d  20916  lssacs  20920  prdsvscacl  20921  lmodvsinv  20990  lmodvsinv2  20991  islmhm2  20992  0lmhm  20994  idlmhm  20995  lmhmco  20997  lmhmplusg  20998  lmhmvsca  20999  lmhmf1o  21000  lmhmpreima  21002  lmhmeql  21009  pwsdiaglmhm  21011  pwssplit3  21015  lvecvscan  21068  lvecvscan2  21069  lspsnvs  21071  lspfixed  21085  lspexch  21086  lspsolvlem  21099  lspsolv  21100  islbs2  21111  ipass  21602  ipassr  21603  phlssphl  21616  ocvlss  21629  dsmmlss  21701  frlmvscavalb  21727  frlmvplusgscavalb  21728  frlmphl  21738  uvcresum  21750  frlmssuvc2  21752  frlmup1  21755  lindfmm  21784  islindf4  21795  assa2ass  21820  assapropd  21828  asclf  21838  assamulgscmlem1  21856  assamulgscmlem2  21857  mplcoe1  21993  mplmon2cl  22024  mplmon2mul  22025  mplind  22026  ply1tmcl  22215  ply1coe  22241  evl1gsummon  22308  evls1fpws  22312  evls1vsca  22316  asclply1subcl  22317  evls1maplmhm  22320  matvscl  22374  mat0dimscm  22412  matinv  22620  mply1topmatcl  22748  pm2mpmhmlem2  22762  monmat2matmon  22767  chpmat1dlem  22778  chpmat1d  22779  chpdmatlem0  22780  chfacfscmulcl  22800  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  cpmadugsumfi  22820  cpmidgsum2  22822  nlmdsdi  24624  nlmdsdir  24625  nlmmul0or  24626  nlmvscnlem2  24628  nlmvscn  24630  clmvscl  25033  cmodscmulexp  25067  cph2ass  25158  ipcau2  25179  tcphcphlem2  25181  tcphcph  25182  cphipval2  25186  4cphipval2  25187  cphipval  25188  pjthlem1  25382  mdegvscale  26021  mdegvsca  26022  plypf1  26158  ttgcontlem1  28941  lmodvslmhm  33116  eqgvscpbl  33415  qusvscpbl  33416  qusvsval  33417  imaslmod  33418  linds2eq  33446  lmhmqusker  33482  ply1degltlss  33661  gsummoncoe1fzo  33662  tngdim  33763  matdim  33765  lindsunlem  33774  lbsdiflsp0  33776  fedgmullem1  33779  fedgmullem2  33780  sitgclbn  34493  lindsadd  37925  lindsenlbs  37927  lfl0  39502  lflsub  39504  lflmul  39505  lfl0f  39506  lfl1  39507  lfladdcl  39508  lflnegcl  39512  lflvscl  39514  lkrlss  39532  eqlkr  39536  lkrlsp  39539  lshpkrlem4  39550  lshpkrlem5  39551  lshpkrlem6  39552  lclkrlem2m  41956  lclkrlem2p  41959  lcdvscl  42042  baerlem3lem1  42144  baerlem5alem1  42145  baerlem5blem1  42146  hdmap14lem1a  42303  hdmap14lem2a  42304  hdmap14lem2N  42306  hdmap14lem3  42307  hdmap14lem4a  42308  hdmap14lem8  42312  hgmapadd  42331  hgmapmul  42332  hgmaprnlem4N  42336  hgmap11  42339  hdmapgln2  42349  hdmapinvlem3  42357  hdmapinvlem4  42358  hdmapglem7b  42365  hlhilphllem  42396  mendassa  43621  ply1mulgsum  48824  lincfsuppcl  48847  linccl  48848  lincvalsng  48850  lincvalpr  48852  lincdifsn  48858  linc1  48859  lincsum  48863  lincscm  48864  lincscmcl  48866  lincext3  48890  lindslinindimp2lem4  48895  lindslinindsimp2  48897  snlindsntor  48905  lincresunit3lem2  48914  lincresunit3  48915  zlmodzxzldeplem3  48936