Theorem lmodvscl 20813

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  +_gcplusg 17163  ._rcmulr 17164  Scalarcsca 17166   ·_𝑠 cvsca 17167  1_rcur 20101  LModclmod 20795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-lmod 20797

This theorem is referenced by:  lmodvscld  20814  lmodscaf  20819  lmod0vs  20830  lmodvsmmulgdi  20832  lcomf  20836  lmodvneg1  20840  lmodvsneg  20841  lmodnegadd  20846  lmodsubvs  20853  lmodsubdi  20854  lmodsubdir  20855  lmodvsghm  20858  lmodprop2d  20859  lss1  20873  lssvsubcl  20879  lssvscl  20890  lss1d  20898  lssacs  20902  prdsvscacl  20903  lmodvsinv  20972  lmodvsinv2  20973  islmhm2  20974  0lmhm  20976  idlmhm  20977  lmhmco  20979  lmhmplusg  20980  lmhmvsca  20981  lmhmf1o  20982  lmhmpreima  20984  lmhmeql  20991  pwsdiaglmhm  20993  pwssplit3  20997  lvecvscan  21050  lvecvscan2  21051  lspsnvs  21053  lspfixed  21067  lspexch  21068  lspsolvlem  21081  lspsolv  21082  islbs2  21093  ipass  21584  ipassr  21585  phlssphl  21598  ocvlss  21611  dsmmlss  21683  frlmvscavalb  21709  frlmvplusgscavalb  21710  frlmphl  21720  uvcresum  21732  frlmssuvc2  21734  frlmup1  21737  lindfmm  21766  islindf4  21777  assa2ass  21802  assapropd  21811  asclf  21821  assamulgscmlem1  21838  assamulgscmlem2  21839  mplcoe1  21973  mplmon2cl  22004  mplmon2mul  22005  mplind  22006  ply1tmcl  22187  ply1coe  22214  evl1gsummon  22281  evls1fpws  22285  evls1vsca  22289  asclply1subcl  22290  evls1maplmhm  22293  matvscl  22347  mat0dimscm  22385  matinv  22593  mply1topmatcl  22721  pm2mpmhmlem2  22735  monmat2matmon  22740  chpmat1dlem  22751  chpmat1d  22752  chpdmatlem0  22753  chfacfscmulcl  22773  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  cpmadugsumfi  22793  cpmidgsum2  22795  nlmdsdi  24597  nlmdsdir  24598  nlmmul0or  24599  nlmvscnlem2  24601  nlmvscn  24603  clmvscl  25016  cmodscmulexp  25050  cph2ass  25141  ipcau2  25162  tcphcphlem2  25164  tcphcph  25165  cphipval2  25169  4cphipval2  25170  cphipval  25171  pjthlem1  25365  mdegvscale  26008  mdegvsca  26009  plypf1  26145  ttgcontlem1  28864  lmodvslmhm  33037  eqgvscpbl  33322  qusvscpbl  33323  qusvsval  33324  imaslmod  33325  linds2eq  33353  lmhmqusker  33389  ply1degltlss  33564  gsummoncoe1fzo  33565  tngdim  33647  matdim  33649  lindsunlem  33658  lbsdiflsp0  33660  fedgmullem1  33663  fedgmullem2  33664  sitgclbn  34377  lindsadd  37673  lindsenlbs  37675  lfl0  39184  lflsub  39186  lflmul  39187  lfl0f  39188  lfl1  39189  lfladdcl  39190  lflnegcl  39194  lflvscl  39196  lkrlss  39214  eqlkr  39218  lkrlsp  39221  lshpkrlem4  39232  lshpkrlem5  39233  lshpkrlem6  39234  lclkrlem2m  41638  lclkrlem2p  41641  lcdvscl  41724  baerlem3lem1  41826  baerlem5alem1  41827  baerlem5blem1  41828  hdmap14lem1a  41985  hdmap14lem2a  41986  hdmap14lem2N  41988  hdmap14lem3  41989  hdmap14lem4a  41990  hdmap14lem8  41994  hgmapadd  42013  hgmapmul  42014  hgmaprnlem4N  42018  hgmap11  42021  hdmapgln2  42031  hdmapinvlem3  42039  hdmapinvlem4  42040  hdmapglem7b  42047  hlhilphllem  42078  mendassa  43307  ply1mulgsum  48515  lincfsuppcl  48538  linccl  48539  lincvalsng  48541  lincvalpr  48543  lincdifsn  48549  linc1  48550  lincsum  48554  lincscm  48555  lincscmcl  48557  lincext3  48581  lindslinindimp2lem4  48586  lindslinindsimp2  48588  snlindsntor  48596  lincresunit3lem2  48605  lincresunit3  48606  zlmodzxzldeplem3  48627