Theorem lmodvscl 20980

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  1_rcur 20264  LModclmod 20962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-lmod 20964

This theorem is referenced by:  lmodvscld  20981  lmodscaf  20986  lmod0vs  20997  lmodvsmmulgdi  20999  lcomf  21003  lmodvneg1  21007  lmodvsneg  21008  lmodnegadd  21013  lmodsubvs  21020  lmodsubdi  21021  lmodsubdir  21022  lmodvsghm  21025  lmodprop2d  21026  lss1  21040  lssvsubcl  21046  lssvscl  21057  lss1d  21065  lssacs  21069  prdsvscacl  21070  lmodvsinv  21138  lmodvsinv2  21139  islmhm2  21140  0lmhm  21142  idlmhm  21143  lmhmco  21145  lmhmplusg  21146  lmhmvsca  21147  lmhmf1o  21148  lmhmpreima  21150  lmhmeql  21157  pwsdiaglmhm  21159  pwssplit3  21163  lvecvscan  21216  lvecvscan2  21217  lspsnvs  21219  lspfixed  21233  lspexch  21234  lspsolvlem  21247  lspsolv  21248  islbs2  21259  ipass  21776  ipassr  21777  phlssphl  21790  ocvlss  21803  dsmmlss  21875  frlmvscavalb  21901  frlmvplusgscavalb  21902  frlmphl  21912  uvcresum  21924  frlmssuvc2  21926  frlmup1  21929  lindfmm  21958  islindf4  21969  assa2ass  21994  assapropd  22002  asclf  22012  assamulgscmlem1  22030  assamulgscmlem2  22031  mplcoe1  22169  mplmon2cl  22200  mplmon2mul  22201  mplind  22202  ply1tmcl  22414  ply1coe  22439  evl1gsummon  22506  evls1fpws  22510  evls1vsca  22514  asclply1subcl  22515  evls1maplmhm  22518  matvscl  22569  mat0dimscm  22607  matinv  22815  mply1topmatcl  22943  pm2mpmhmlem2  22957  monmat2matmon  22962  chpmat1dlem  22973  chpmat1d  22974  chpdmatlem0  22975  chfacfscmulcl  22995  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  cpmadugsumfi  23015  cpmidgsum2  23017  nlmdsdi  24819  nlmdsdir  24820  nlmmul0or  24821  nlmvscnlem2  24823  nlmvscn  24825  clmvscl  25228  cmodscmulexp  25262  cph2ass  25353  ipcau2  25374  tcphcphlem2  25376  tcphcph  25377  cphipval2  25381  4cphipval2  25382  cphipval  25383  pjthlem1  25577  mdegvscale  26213  mdegvsca  26214  plypf1  26350  ttgcontlem1  29212  lmodvslmhm  33348  eqgvscpbl  33648  qusvscpbl  33649  qusvsval  33650  imaslmod  33651  linds2eq  33672  lmhmqusker  33704  ply1degltlss  33864  gsummoncoe1fzo  33865  tngdim  33981  matdim  33983  lindsunlem  33992  lbsdiflsp0  33994  fedgmullem1  33997  fedgmullem2  33998  sitgclbn  34711  lindsadd  38242  lindsenlbs  38244  lfl0  39817  lflsub  39819  lflmul  39820  lfl0f  39821  lfl1  39822  lfladdcl  39823  lflnegcl  39827  lflvscl  39829  lkrlss  39847  eqlkr  39851  lkrlsp  39854  lshpkrlem4  39865  lshpkrlem5  39866  lshpkrlem6  39867  lclkrlem2m  42271  lclkrlem2p  42274  lcdvscl  42357  baerlem3lem1  42459  baerlem5alem1  42460  baerlem5blem1  42461  hdmap14lem1a  42618  hdmap14lem2a  42619  hdmap14lem2N  42621  hdmap14lem3  42622  hdmap14lem4a  42623  hdmap14lem8  42627  hgmapadd  42646  hgmapmul  42647  hgmaprnlem4N  42651  hgmap11  42654  hdmapgln2  42664  hdmapinvlem3  42672  hdmapinvlem4  42673  hdmapglem7b  42680  hlhilphllem  42711  mendassa  43897  ply1mulgsum  49147  lincfsuppcl  49170  linccl  49171  lincvalsng  49173  lincvalpr  49175  lincdifsn  49181  linc1  49182  lincsum  49186  lincscm  49187  lincscmcl  49189  lincext3  49213  lindslinindimp2lem4  49218  lindslinindsimp2  49220  snlindsntor  49228  lincresunit3lem2  49237  lincresunit3  49238  zlmodzxzldeplem3  49259