Theorem lmodvscl 18703

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  1_rcur 18324  LModclmod 18686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-lmod 18688

This theorem is referenced by:  lmodscaf  18708  lmod0vs  18719  lmodvsmmulgdi  18721  lcomf  18725  lmodvneg1  18729  lmodvsneg  18730  lmodnegadd  18735  lmodsubvs  18742  lmodsubdi  18743  lmodsubdir  18744  lmodvsghm  18747  lmodprop2d  18748  lss1  18760  lssvsubcl  18765  lssvscl  18776  lss1d  18784  lssacs  18788  prdsvscacl  18789  lmodvsinv  18857  lmodvsinv2  18858  islmhm2  18859  0lmhm  18861  idlmhm  18862  lmhmco  18864  lmhmplusg  18865  lmhmvsca  18866  lmhmf1o  18867  lmhmpreima  18869  lmhmeql  18876  pwsdiaglmhm  18878  pwssplit3  18882  lvecvscan  18932  lvecvscan2  18933  lspsnvs  18935  lspfixed  18949  lspexch  18950  lspsolvlem  18963  lspsolv  18964  islbs2  18975  assa2ass  19143  assapropd  19148  asclf  19158  asclrhm  19163  assamulgscmlem1  19169  assamulgscmlem2  19170  mplcoe1  19286  mplmon2cl  19321  mplmon2mul  19322  mplind  19323  ply1tmcl  19463  ply1coe  19487  evl1gsummon  19550  ipass  19809  ipassr  19810  ocvlss  19835  dsmmlss  19907  frlmphl  19939  uvcresum  19951  frlmssuvc2  19953  frlmup1  19956  lindfmm  19985  islindf4  19996  matvscl  20056  mat0dimscm  20094  matinv  20302  mply1topmatcl  20429  pm2mpmhmlem2  20443  monmat2matmon  20448  chpmat1dlem  20459  chpmat1d  20460  chpdmatlem0  20461  chfacfscmulcl  20481  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmidgsum2  20503  nlmdsdi  22295  nlmdsdir  22296  nlmmul0or  22297  nlmvscnlem2  22299  nlmvscn  22301  clmvscl  22696  cmodscmulexp  22730  cph2ass  22821  ipcau2  22841  tchcphlem2  22843  tchcph  22844  cphipval2  22848  4cphipval2  22849  cphipval  22850  pjthlem1  23016  mdegvscale  23639  mdegvsca  23640  plypf1  23772  ttgcontlem1  25565  sitgclbn  29732  lindsenlbs  32574  lfl0  33370  lflsub  33372  lflmul  33373  lfl0f  33374  lfl1  33375  lfladdcl  33376  lflnegcl  33380  lflvscl  33382  lkrlss  33400  eqlkr  33404  lkrlsp  33407  lshpkrlem4  33418  lshpkrlem5  33419  lshpkrlem6  33420  lclkrlem2m  35826  lclkrlem2p  35829  lcdvscl  35912  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  hdmap14lem1a  36176  hdmap14lem2a  36177  hdmap14lem2N  36179  hdmap14lem3  36180  hdmap14lem4a  36181  hdmap14lem8  36185  hgmapadd  36204  hgmapmul  36205  hgmaprnlem4N  36209  hgmap11  36212  hdmapgln2  36222  hdmapinvlem3  36230  hdmapinvlem4  36231  hdmapglem7b  36238  hlhilphllem  36269  mendassa  36783  ply1mulgsum  41972  lincfsuppcl  41996  linccl  41997  lincvalsng  41999  lincvalpr  42001  lincdifsn  42007  linc1  42008  lincsum  42012  lincscm  42013  lincscmcl  42015  lincext3  42039  lindslinindimp2lem4  42044  lindslinindsimp2  42046  snlindsntor  42054  lincresunit3lem2  42063  lincresunit3  42064  zlmodzxzldeplem3  42085