Theorem lmodvscl 20892

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  1_rcur 20198  LModclmod 20874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-lmod 20876

This theorem is referenced by:  lmodvscld  20893  lmodscaf  20898  lmod0vs  20909  lmodvsmmulgdi  20911  lcomf  20915  lmodvneg1  20919  lmodvsneg  20920  lmodnegadd  20925  lmodsubvs  20932  lmodsubdi  20933  lmodsubdir  20934  lmodvsghm  20937  lmodprop2d  20938  lss1  20953  lssvsubcl  20959  lssvscl  20970  lss1d  20978  lssacs  20982  prdsvscacl  20983  lmodvsinv  21052  lmodvsinv2  21053  islmhm2  21054  0lmhm  21056  idlmhm  21057  lmhmco  21059  lmhmplusg  21060  lmhmvsca  21061  lmhmf1o  21062  lmhmpreima  21064  lmhmeql  21071  pwsdiaglmhm  21073  pwssplit3  21077  lvecvscan  21130  lvecvscan2  21131  lspsnvs  21133  lspfixed  21147  lspexch  21148  lspsolvlem  21161  lspsolv  21162  islbs2  21173  ipass  21680  ipassr  21681  phlssphl  21694  ocvlss  21707  dsmmlss  21781  frlmvscavalb  21807  frlmvplusgscavalb  21808  frlmphl  21818  uvcresum  21830  frlmssuvc2  21832  frlmup1  21835  lindfmm  21864  islindf4  21875  assa2ass  21900  assapropd  21909  asclf  21919  assamulgscmlem1  21936  assamulgscmlem2  21937  mplcoe1  22072  mplmon2cl  22109  mplmon2mul  22110  mplind  22111  ply1tmcl  22290  ply1coe  22317  evl1gsummon  22384  evls1fpws  22388  evls1vsca  22392  asclply1subcl  22393  evls1maplmhm  22396  matvscl  22452  mat0dimscm  22490  matinv  22698  mply1topmatcl  22826  pm2mpmhmlem2  22840  monmat2matmon  22845  chpmat1dlem  22856  chpmat1d  22857  chpdmatlem0  22858  chfacfscmulcl  22878  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmidgsum2  22900  nlmdsdi  24717  nlmdsdir  24718  nlmmul0or  24719  nlmvscnlem2  24721  nlmvscn  24723  clmvscl  25134  cmodscmulexp  25168  cph2ass  25260  ipcau2  25281  tcphcphlem2  25283  tcphcph  25284  cphipval2  25288  4cphipval2  25289  cphipval  25290  pjthlem1  25484  mdegvscale  26128  mdegvsca  26129  plypf1  26265  ttgcontlem1  28913  lmodvslmhm  33035  eqgvscpbl  33357  qusvscpbl  33358  qusvsval  33359  imaslmod  33360  linds2eq  33388  lmhmqusker  33424  ply1degltlss  33596  gsummoncoe1fzo  33597  tngdim  33640  matdim  33642  lindsunlem  33651  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  sitgclbn  34324  lindsadd  37599  lindsenlbs  37601  lfl0  39046  lflsub  39048  lflmul  39049  lfl0f  39050  lfl1  39051  lfladdcl  39052  lflnegcl  39056  lflvscl  39058  lkrlss  39076  eqlkr  39080  lkrlsp  39083  lshpkrlem4  39094  lshpkrlem5  39095  lshpkrlem6  39096  lclkrlem2m  41501  lclkrlem2p  41504  lcdvscl  41587  baerlem3lem1  41689  baerlem5alem1  41690  baerlem5blem1  41691  hdmap14lem1a  41848  hdmap14lem2a  41849  hdmap14lem2N  41851  hdmap14lem3  41852  hdmap14lem4a  41853  hdmap14lem8  41857  hgmapadd  41876  hgmapmul  41877  hgmaprnlem4N  41881  hgmap11  41884  hdmapgln2  41894  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem7b  41910  hlhilphllem  41945  mendassa  43178  ply1mulgsum  48235  lincfsuppcl  48258  linccl  48259  lincvalsng  48261  lincvalpr  48263  lincdifsn  48269  linc1  48270  lincsum  48274  lincscm  48275  lincscmcl  48277  lincext3  48301  lindslinindimp2lem4  48306  lindslinindsimp2  48308  snlindsntor  48316  lincresunit3lem2  48325  lincresunit3  48326  zlmodzxzldeplem3  48347