Theorem lmodvscl 20876

Description: Closure of scalar product for a left module. (hvmulcl 31032 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 20863	. . . 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 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  1_rcur 20178  LModclmod 20858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-lmod 20860

This theorem is referenced by:  lmodvscld  20877  lmodscaf  20882  lmod0vs  20893  lmodvsmmulgdi  20895  lcomf  20899  lmodvneg1  20903  lmodvsneg  20904  lmodnegadd  20909  lmodsubvs  20916  lmodsubdi  20917  lmodsubdir  20918  lmodvsghm  20921  lmodprop2d  20922  lss1  20936  lssvsubcl  20942  lssvscl  20953  lss1d  20961  lssacs  20965  prdsvscacl  20966  lmodvsinv  21035  lmodvsinv2  21036  islmhm2  21037  0lmhm  21039  idlmhm  21040  lmhmco  21042  lmhmplusg  21043  lmhmvsca  21044  lmhmf1o  21045  lmhmpreima  21047  lmhmeql  21054  pwsdiaglmhm  21056  pwssplit3  21060  lvecvscan  21113  lvecvscan2  21114  lspsnvs  21116  lspfixed  21130  lspexch  21131  lspsolvlem  21144  lspsolv  21145  islbs2  21156  ipass  21663  ipassr  21664  phlssphl  21677  ocvlss  21690  dsmmlss  21764  frlmvscavalb  21790  frlmvplusgscavalb  21791  frlmphl  21801  uvcresum  21813  frlmssuvc2  21815  frlmup1  21818  lindfmm  21847  islindf4  21858  assa2ass  21883  assapropd  21892  asclf  21902  assamulgscmlem1  21919  assamulgscmlem2  21920  mplcoe1  22055  mplmon2cl  22092  mplmon2mul  22093  mplind  22094  ply1tmcl  22275  ply1coe  22302  evl1gsummon  22369  evls1fpws  22373  evls1vsca  22377  asclply1subcl  22378  evls1maplmhm  22381  matvscl  22437  mat0dimscm  22475  matinv  22683  mply1topmatcl  22811  pm2mpmhmlem2  22825  monmat2matmon  22830  chpmat1dlem  22841  chpmat1d  22842  chpdmatlem0  22843  chfacfscmulcl  22863  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cpmadugsumfi  22883  cpmidgsum2  22885  nlmdsdi  24702  nlmdsdir  24703  nlmmul0or  24704  nlmvscnlem2  24706  nlmvscn  24708  clmvscl  25121  cmodscmulexp  25155  cph2ass  25247  ipcau2  25268  tcphcphlem2  25270  tcphcph  25271  cphipval2  25275  4cphipval2  25276  cphipval  25277  pjthlem1  25471  mdegvscale  26114  mdegvsca  26115  plypf1  26251  ttgcontlem1  28899  lmodvslmhm  33053  eqgvscpbl  33378  qusvscpbl  33379  qusvsval  33380  imaslmod  33381  linds2eq  33409  lmhmqusker  33445  ply1degltlss  33617  gsummoncoe1fzo  33618  tngdim  33664  matdim  33666  lindsunlem  33675  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  sitgclbn  34345  lindsadd  37620  lindsenlbs  37622  lfl0  39066  lflsub  39068  lflmul  39069  lfl0f  39070  lfl1  39071  lfladdcl  39072  lflnegcl  39076  lflvscl  39078  lkrlss  39096  eqlkr  39100  lkrlsp  39103  lshpkrlem4  39114  lshpkrlem5  39115  lshpkrlem6  39116  lclkrlem2m  41521  lclkrlem2p  41524  lcdvscl  41607  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  hdmap14lem1a  41868  hdmap14lem2a  41869  hdmap14lem2N  41871  hdmap14lem3  41872  hdmap14lem4a  41873  hdmap14lem8  41877  hgmapadd  41896  hgmapmul  41897  hgmaprnlem4N  41901  hgmap11  41904  hdmapgln2  41914  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem7b  41930  hlhilphllem  41965  mendassa  43202  ply1mulgsum  48307  lincfsuppcl  48330  linccl  48331  lincvalsng  48333  lincvalpr  48335  lincdifsn  48341  linc1  48342  lincsum  48346  lincscm  48347  lincscmcl  48349  lincext3  48373  lindslinindimp2lem4  48378  lindslinindsimp2  48380  snlindsntor  48388  lincresunit3lem2  48397  lincresunit3  48398  zlmodzxzldeplem3  48419