Theorem lmodvscl 21036

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  ._rcmulr 17336  Scalarcsca 17338   ·_𝑠 cvsca 17339  1_rcur 20294  LModclmod 21018

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-lmod 21020

This theorem is used by:  lmodvscld  21037  lmodscaf  21042  lmod0vs  21053  lmodvsmmulgdi  21055  lcomf  21059  lmodvneg1  21063  lmodvsneg  21064  lmodnegadd  21069  lmodsubvs  21076  lmodsubdi  21077  lmodsubdir  21078  lmodvsghm  21081  lmodprop2d  21082  lss1  21096  lssvsubcl  21102  lssvscl  21113  lss1d  21121  lssacs  21125  prdsvscacl  21126  lmodvsinv  21194  lmodvsinv2  21195  islmhm2  21196  0lmhm  21198  idlmhm  21199  lmhmco  21201  lmhmplusg  21202  lmhmvsca  21203  lmhmf1o  21204  lmhmpreima  21206  lmhmeql  21213  pwsdiaglmhm  21215  pwssplit3  21219  lvecvscan  21272  lvecvscan2  21273  lspsnvs  21275  lspfixed  21289  lspexch  21290  lspsolvlem  21303  lspsolv  21304  islbs2  21315  ipass  21832  ipassr  21833  phlssphl  21846  ocvlss  21859  dsmmlss  21931  frlmvscavalb  21957  frlmvplusgscavalb  21958  frlmphl  21968  uvcresum  21980  frlmssuvc2  21982  frlmup1  21985  lindfmm  22014  islindf4  22025  assa2ass  22050  assapropd  22058  asclf  22068  assamulgscmlem1  22086  assamulgscmlem2  22087  mplcoe1  22225  mplmon2cl  22256  mplmon2mul  22257  mplind  22258  ply1tmcl  22470  ply1coe  22495  evl1gsummon  22562  evls1fpws  22566  evls1vsca  22570  asclply1subcl  22571  evls1maplmhm  22574  matvscl  22625  mat0dimscm  22663  matinv  22871  mply1topmatcl  22999  pm2mpmhmlem2  23013  monmat2matmon  23018  chpmat1dlem  23029  chpmat1d  23030  chpdmatlem0  23031  chfacfscmulcl  23051  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  cpmadugsumfi  23071  cpmidgsum2  23073  nlmdsdi  24875  nlmdsdir  24876  nlmmul0or  24877  nlmvscnlem2  24879  nlmvscn  24881  clmvscl  25284  cmodscmulexp  25318  cph2ass  25409  ipcau2  25430  tcphcphlem2  25432  tcphcph  25433  cphipval2  25437  4cphipval2  25438  cphipval  25439  pjthlem1  25633  mdegvscale  26269  mdegvsca  26270  plypf1  26406  ttgcontlem1  29271  lmodvslmhm  33401  eqgvscpbl  33701  qusvscpbl  33702  qusvsval  33703  imaslmod  33704  linds2eq  33725  lmhmqusker  33757  ply1degltlss  33917  gsummoncoe1fzo  33918  tngdim  34034  matdim  34036  lindsunlem  34045  lbsdiflsp0  34047  fedgmullem1  34050  fedgmullem2  34051  sitgclbn  34764  lindsadd  38304  lindsenlbs  38306  lfl0  39879  lflsub  39881  lflmul  39882  lfl0f  39883  lfl1  39884  lfladdcl  39885  lflnegcl  39889  lflvscl  39891  lkrlss  39909  eqlkr  39913  lkrlsp  39916  lshpkrlem4  39927  lshpkrlem5  39928  lshpkrlem6  39929  lclkrlem2m  42333  lclkrlem2p  42336  lcdvscl  42419  baerlem3lem1  42521  baerlem5alem1  42522  baerlem5blem1  42523  hdmap14lem1a  42680  hdmap14lem2a  42681  hdmap14lem2N  42683  hdmap14lem3  42684  hdmap14lem4a  42685  hdmap14lem8  42689  hgmapadd  42708  hgmapmul  42709  hgmaprnlem4N  42713  hgmap11  42716  hdmapgln2  42726  hdmapinvlem3  42734  hdmapinvlem4  42735  hdmapglem7b  42742  hlhilphllem  42773  mendassa  43957  ply1mulgsum  49210  lincfsuppcl  49233  linccl  49234  lincvalsng  49236  lincvalpr  49238  lincdifsn  49244  linc1  49245  lincsum  49249  lincscm  49250  lincscmcl  49252  lincext3  49276  lindslinindimp2lem4  49281  lindslinindsimp2  49283  snlindsntor  49291  lincresunit3lem2  49300  lincresunit3  49301  zlmodzxzldeplem3  49322