Theorem lmodvscl 20149

Description: Closure of scalar product for a left module. (hvmulcl 29384 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 260	. 2 ⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2		pm4.24 564	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 564	. 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 20137	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 495	. . 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 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  +_gcplusg 16971  ._rcmulr 16972  Scalarcsca 16974   ·_𝑠 cvsca 16975  1_rcur 19746  LModclmod 20132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-lmod 20134

This theorem is referenced by:  lmodscaf  20154  lmod0vs  20165  lmodvsmmulgdi  20167  lcomf  20171  lmodvneg1  20175  lmodvsneg  20176  lmodnegadd  20181  lmodsubvs  20188  lmodsubdi  20189  lmodsubdir  20190  lmodvsghm  20193  lmodprop2d  20194  lss1  20209  lssvsubcl  20214  lssvscl  20226  lss1d  20234  lssacs  20238  prdsvscacl  20239  lmodvsinv  20307  lmodvsinv2  20308  islmhm2  20309  0lmhm  20311  idlmhm  20312  lmhmco  20314  lmhmplusg  20315  lmhmvsca  20316  lmhmf1o  20317  lmhmpreima  20319  lmhmeql  20326  pwsdiaglmhm  20328  pwssplit3  20332  lvecvscan  20382  lvecvscan2  20383  lspsnvs  20385  lspfixed  20399  lspexch  20400  lspsolvlem  20413  lspsolv  20414  islbs2  20425  ipass  20859  ipassr  20860  phlssphl  20873  ocvlss  20886  dsmmlss  20960  frlmvscavalb  20986  frlmvplusgscavalb  20987  frlmphl  20997  uvcresum  21009  frlmssuvc2  21011  frlmup1  21014  lindfmm  21043  islindf4  21054  assa2ass  21079  assapropd  21085  asclf  21095  assamulgscmlem1  21112  assamulgscmlem2  21113  mplcoe1  21247  mplmon2cl  21285  mplmon2mul  21286  mplind  21287  mhpvscacl  21353  ply1tmcl  21452  ply1coe  21476  evl1gsummon  21540  matvscl  21589  mat0dimscm  21627  matinv  21835  mply1topmatcl  21963  pm2mpmhmlem2  21977  monmat2matmon  21982  chpmat1dlem  21993  chpmat1d  21994  chpdmatlem0  21995  chfacfscmulcl  22015  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  cpmadugsumfi  22035  cpmidgsum2  22037  nlmdsdi  23854  nlmdsdir  23855  nlmmul0or  23856  nlmvscnlem2  23858  nlmvscn  23860  clmvscl  24260  cmodscmulexp  24294  cph2ass  24386  ipcau2  24407  tcphcphlem2  24409  tcphcph  24410  cphipval2  24414  4cphipval2  24415  cphipval  24416  pjthlem1  24610  mdegvscale  25249  mdegvsca  25250  plypf1  25382  ttgcontlem1  27261  lmodvslmhm  31319  eqgvscpbl  31559  qusvscpbl  31560  qusscaval  31561  imaslmod  31562  linds2eq  31584  tngdim  31705  matdim  31707  lindsunlem  31714  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  sitgclbn  32319  lindsadd  35779  lindsenlbs  35781  lfl0  37086  lflsub  37088  lflmul  37089  lfl0f  37090  lfl1  37091  lfladdcl  37092  lflnegcl  37096  lflvscl  37098  lkrlss  37116  eqlkr  37120  lkrlsp  37123  lshpkrlem4  37134  lshpkrlem5  37135  lshpkrlem6  37136  lclkrlem2m  39540  lclkrlem2p  39543  lcdvscl  39626  baerlem3lem1  39728  baerlem5alem1  39729  baerlem5blem1  39730  hdmap14lem1a  39887  hdmap14lem2a  39888  hdmap14lem2N  39890  hdmap14lem3  39891  hdmap14lem4a  39892  hdmap14lem8  39896  hgmapadd  39915  hgmapmul  39916  hgmaprnlem4N  39920  hgmap11  39923  hdmapgln2  39933  hdmapinvlem3  39941  hdmapinvlem4  39942  hdmapglem7b  39949  hlhilphllem  39984  frlmsnic  40270  prjspvs  40456  prjspeclsp  40458  mendassa  41026  ply1mulgsum  45742  lincfsuppcl  45765  linccl  45766  lincvalsng  45768  lincvalpr  45770  lincdifsn  45776  linc1  45777  lincsum  45781  lincscm  45782  lincscmcl  45784  lincext3  45808  lindslinindimp2lem4  45813  lindslinindsimp2  45815  snlindsntor  45823  lincresunit3lem2  45832  lincresunit3  45833  zlmodzxzldeplem3  45854