Theorem lmodvscl 19654

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  +_gcplusg 16568  ._rcmulr 16569  Scalarcsca 16571   ·_𝑠 cvsca 16572  1_rcur 19254  LModclmod 19637

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-nul 5213

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-lmod 19639

This theorem is referenced by:  lmodscaf  19659  lmod0vs  19670  lmodvsmmulgdi  19672  lcomf  19676  lmodvneg1  19680  lmodvsneg  19681  lmodnegadd  19686  lmodsubvs  19693  lmodsubdi  19694  lmodsubdir  19695  lmodvsghm  19698  lmodprop2d  19699  lss1  19713  lssvsubcl  19718  lssvscl  19730  lss1d  19738  lssacs  19742  prdsvscacl  19743  lmodvsinv  19811  lmodvsinv2  19812  islmhm2  19813  0lmhm  19815  idlmhm  19816  lmhmco  19818  lmhmplusg  19819  lmhmvsca  19820  lmhmf1o  19821  lmhmpreima  19823  lmhmeql  19830  pwsdiaglmhm  19832  pwssplit3  19836  lvecvscan  19886  lvecvscan2  19887  lspsnvs  19889  lspfixed  19903  lspexch  19904  lspsolvlem  19917  lspsolv  19918  islbs2  19929  assa2ass  20098  assapropd  20104  asclf  20114  ascldimulOLD  20120  assamulgscmlem1  20131  assamulgscmlem2  20132  mplcoe1  20249  mplmon2cl  20283  mplmon2mul  20284  mplind  20285  mhpvscacl  20344  ply1tmcl  20443  ply1coe  20467  evl1gsummon  20531  ipass  20792  ipassr  20793  phlssphl  20806  ocvlss  20819  dsmmlss  20891  frlmvscavalb  20917  frlmvplusgscavalb  20918  frlmphl  20928  uvcresum  20940  frlmssuvc2  20942  frlmup1  20945  lindfmm  20974  islindf4  20985  matvscl  21043  mat0dimscm  21081  matinv  21289  mply1topmatcl  21416  pm2mpmhmlem2  21430  monmat2matmon  21435  chpmat1dlem  21446  chpmat1d  21447  chpdmatlem0  21448  chfacfscmulcl  21468  cpmadugsumlemB  21485  cpmadugsumlemC  21486  cpmadugsumlemF  21487  cpmadugsumfi  21488  cpmidgsum2  21490  nlmdsdi  23293  nlmdsdir  23294  nlmmul0or  23295  nlmvscnlem2  23297  nlmvscn  23299  clmvscl  23695  cmodscmulexp  23729  cph2ass  23820  ipcau2  23840  tcphcphlem2  23842  tcphcph  23843  cphipval2  23847  4cphipval2  23848  cphipval  23849  pjthlem1  24043  mdegvscale  24672  mdegvsca  24673  plypf1  24805  ttgcontlem1  26674  lmodvslmhm  30692  eqgvscpbl  30923  qusvscpbl  30924  qusscaval  30925  imaslmod  30926  linds2eq  30945  tngdim  31015  matdim  31017  lindsunlem  31024  lbsdiflsp0  31026  fedgmullem1  31029  fedgmullem2  31030  sitgclbn  31605  lindsadd  34889  lindsenlbs  34891  lfl0  36205  lflsub  36207  lflmul  36208  lfl0f  36209  lfl1  36210  lfladdcl  36211  lflnegcl  36215  lflvscl  36217  lkrlss  36235  eqlkr  36239  lkrlsp  36242  lshpkrlem4  36253  lshpkrlem5  36254  lshpkrlem6  36255  lclkrlem2m  38659  lclkrlem2p  38662  lcdvscl  38745  baerlem3lem1  38847  baerlem5alem1  38848  baerlem5blem1  38849  hdmap14lem1a  39006  hdmap14lem2a  39007  hdmap14lem2N  39009  hdmap14lem3  39010  hdmap14lem4a  39011  hdmap14lem8  39015  hgmapadd  39034  hgmapmul  39035  hgmaprnlem4N  39039  hgmap11  39042  hdmapgln2  39052  hdmapinvlem3  39060  hdmapinvlem4  39061  hdmapglem7b  39068  hlhilphllem  39099  frlmsnic  39155  prjspvs  39266  prjspeclsp  39268  mendassa  39800  ply1mulgsum  44451  lincfsuppcl  44475  linccl  44476  lincvalsng  44478  lincvalpr  44480  lincdifsn  44486  linc1  44487  lincsum  44491  lincscm  44492  lincscmcl  44494  lincext3  44518  lindslinindimp2lem4  44523  lindslinindsimp2  44525  snlindsntor  44533  lincresunit3lem2  44542  lincresunit3  44543  zlmodzxzldeplem3  44564