Theorem lmodvscl 19783

Description: Closure of scalar product for a left module. (hvmulcl 28961 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 567	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 567	. 2 ⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4		lmodvscl.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2739	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2739	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2739	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2739	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 19771	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 498	. . 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 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ‘cfv 6350  (class class class)co 7183  Basecbs 16599  +_gcplusg 16681  ._rcmulr 16682  Scalarcsca 16684   ·_𝑠 cvsca 16685  1_rcur 19383  LModclmod 19766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-sbc 3686  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-iota 6308  df-fv 6358  df-ov 7186  df-lmod 19768

This theorem is referenced by:  lmodscaf  19788  lmod0vs  19799  lmodvsmmulgdi  19801  lcomf  19805  lmodvneg1  19809  lmodvsneg  19810  lmodnegadd  19815  lmodsubvs  19822  lmodsubdi  19823  lmodsubdir  19824  lmodvsghm  19827  lmodprop2d  19828  lss1  19842  lssvsubcl  19847  lssvscl  19859  lss1d  19867  lssacs  19871  prdsvscacl  19872  lmodvsinv  19940  lmodvsinv2  19941  islmhm2  19942  0lmhm  19944  idlmhm  19945  lmhmco  19947  lmhmplusg  19948  lmhmvsca  19949  lmhmf1o  19950  lmhmpreima  19952  lmhmeql  19959  pwsdiaglmhm  19961  pwssplit3  19965  lvecvscan  20015  lvecvscan2  20016  lspsnvs  20018  lspfixed  20032  lspexch  20033  lspsolvlem  20046  lspsolv  20047  islbs2  20058  ipass  20474  ipassr  20475  phlssphl  20488  ocvlss  20501  dsmmlss  20573  frlmvscavalb  20599  frlmvplusgscavalb  20600  frlmphl  20610  uvcresum  20622  frlmssuvc2  20624  frlmup1  20627  lindfmm  20656  islindf4  20667  assa2ass  20692  assapropd  20698  asclf  20708  ascldimulOLD  20715  assamulgscmlem1  20726  assamulgscmlem2  20727  mplcoe1  20861  mplmon2cl  20893  mplmon2mul  20894  mplind  20895  mhpvscacl  20961  ply1tmcl  21060  ply1coe  21084  evl1gsummon  21148  matvscl  21195  mat0dimscm  21233  matinv  21441  mply1topmatcl  21569  pm2mpmhmlem2  21583  monmat2matmon  21588  chpmat1dlem  21599  chpmat1d  21600  chpdmatlem0  21601  chfacfscmulcl  21621  cpmadugsumlemB  21638  cpmadugsumlemC  21639  cpmadugsumlemF  21640  cpmadugsumfi  21641  cpmidgsum2  21643  nlmdsdi  23447  nlmdsdir  23448  nlmmul0or  23449  nlmvscnlem2  23451  nlmvscn  23453  clmvscl  23853  cmodscmulexp  23887  cph2ass  23978  ipcau2  23999  tcphcphlem2  24001  tcphcph  24002  cphipval2  24006  4cphipval2  24007  cphipval  24008  pjthlem1  24202  mdegvscale  24841  mdegvsca  24842  plypf1  24974  ttgcontlem1  26844  lmodvslmhm  30900  eqgvscpbl  31135  qusvscpbl  31136  qusscaval  31137  imaslmod  31138  linds2eq  31160  tngdim  31281  matdim  31283  lindsunlem  31290  lbsdiflsp0  31292  fedgmullem1  31295  fedgmullem2  31296  sitgclbn  31893  lindsadd  35426  lindsenlbs  35428  lfl0  36735  lflsub  36737  lflmul  36738  lfl0f  36739  lfl1  36740  lfladdcl  36741  lflnegcl  36745  lflvscl  36747  lkrlss  36765  eqlkr  36769  lkrlsp  36772  lshpkrlem4  36783  lshpkrlem5  36784  lshpkrlem6  36785  lclkrlem2m  39189  lclkrlem2p  39192  lcdvscl  39275  baerlem3lem1  39377  baerlem5alem1  39378  baerlem5blem1  39379  hdmap14lem1a  39536  hdmap14lem2a  39537  hdmap14lem2N  39539  hdmap14lem3  39540  hdmap14lem4a  39541  hdmap14lem8  39545  hgmapadd  39564  hgmapmul  39565  hgmaprnlem4N  39569  hgmap11  39572  hdmapgln2  39582  hdmapinvlem3  39590  hdmapinvlem4  39591  hdmapglem7b  39598  hlhilphllem  39629  frlmsnic  39885  prjspvs  40067  prjspeclsp  40069  mendassa  40632  ply1mulgsum  45313  lincfsuppcl  45336  linccl  45337  lincvalsng  45339  lincvalpr  45341  lincdifsn  45347  linc1  45348  lincsum  45352  lincscm  45353  lincscmcl  45355  lincext3  45379  lindslinindimp2lem4  45384  lindslinindsimp2  45386  snlindsntor  45394  lincresunit3lem2  45403  lincresunit3  45404  zlmodzxzldeplem3  45425