Theorem lmodvscl 20968

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  Scalarcsca 17303   ·_𝑠 cvsca 17304  1_rcur 20254  LModclmod 20950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-lmod 20952

This theorem is referenced by:  lmodvscld  20969  lmodscaf  20974  lmod0vs  20985  lmodvsmmulgdi  20987  lcomf  20991  lmodvneg1  20995  lmodvsneg  20996  lmodnegadd  21001  lmodsubvs  21008  lmodsubdi  21009  lmodsubdir  21010  lmodvsghm  21013  lmodprop2d  21014  lss1  21028  lssvsubcl  21034  lssvscl  21045  lss1d  21053  lssacs  21057  prdsvscacl  21058  lmodvsinv  21126  lmodvsinv2  21127  islmhm2  21128  0lmhm  21130  idlmhm  21131  lmhmco  21133  lmhmplusg  21134  lmhmvsca  21135  lmhmf1o  21136  lmhmpreima  21138  lmhmeql  21145  pwsdiaglmhm  21147  pwssplit3  21151  lvecvscan  21204  lvecvscan2  21205  lspsnvs  21207  lspfixed  21221  lspexch  21222  lspsolvlem  21235  lspsolv  21236  islbs2  21247  ipass  21755  ipassr  21756  phlssphl  21769  ocvlss  21782  dsmmlss  21854  frlmvscavalb  21880  frlmvplusgscavalb  21881  frlmphl  21891  uvcresum  21903  frlmssuvc2  21905  frlmup1  21908  lindfmm  21937  islindf4  21948  assa2ass  21973  assapropd  21981  asclf  21991  assamulgscmlem1  22009  assamulgscmlem2  22010  mplcoe1  22148  mplmon2cl  22179  mplmon2mul  22180  mplind  22181  ply1tmcl  22393  ply1coe  22419  evl1gsummon  22486  evls1fpws  22490  evls1vsca  22494  asclply1subcl  22495  evls1maplmhm  22498  matvscl  22549  mat0dimscm  22587  matinv  22795  mply1topmatcl  22923  pm2mpmhmlem2  22937  monmat2matmon  22942  chpmat1dlem  22953  chpmat1d  22954  chpdmatlem0  22955  chfacfscmulcl  22975  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  cpmadugsumfi  22995  cpmidgsum2  22997  nlmdsdi  24799  nlmdsdir  24800  nlmmul0or  24801  nlmvscnlem2  24803  nlmvscn  24805  clmvscl  25208  cmodscmulexp  25242  cph2ass  25333  ipcau2  25354  tcphcphlem2  25356  tcphcph  25357  cphipval2  25361  4cphipval2  25362  cphipval  25363  pjthlem1  25557  mdegvscale  26193  mdegvsca  26194  plypf1  26330  ttgcontlem1  29143  lmodvslmhm  33283  eqgvscpbl  33585  qusvscpbl  33586  qusvsval  33587  imaslmod  33588  linds2eq  33610  lmhmqusker  33642  ply1degltlss  33803  gsummoncoe1fzo  33804  tngdim  33920  matdim  33922  lindsunlem  33931  lbsdiflsp0  33933  fedgmullem1  33936  fedgmullem2  33937  sitgclbn  34650  lindsadd  38124  lindsenlbs  38126  lfl0  39701  lflsub  39703  lflmul  39704  lfl0f  39705  lfl1  39706  lfladdcl  39707  lflnegcl  39711  lflvscl  39713  lkrlss  39731  eqlkr  39735  lkrlsp  39738  lshpkrlem4  39749  lshpkrlem5  39750  lshpkrlem6  39751  lclkrlem2m  42155  lclkrlem2p  42158  lcdvscl  42241  baerlem3lem1  42343  baerlem5alem1  42344  baerlem5blem1  42345  hdmap14lem1a  42502  hdmap14lem2a  42503  hdmap14lem2N  42505  hdmap14lem3  42506  hdmap14lem4a  42507  hdmap14lem8  42511  hgmapadd  42530  hgmapmul  42531  hgmaprnlem4N  42535  hgmap11  42538  hdmapgln2  42548  hdmapinvlem3  42556  hdmapinvlem4  42557  hdmapglem7b  42564  hlhilphllem  42595  mendassa  43779  ply1mulgsum  49021  lincfsuppcl  49044  linccl  49045  lincvalsng  49047  lincvalpr  49049  lincdifsn  49055  linc1  49056  lincsum  49060  lincscm  49061  lincscmcl  49063  lincext3  49087  lindslinindimp2lem4  49092  lindslinindsimp2  49094  snlindsntor  49102  lincresunit3lem2  49111  lincresunit3  49112  zlmodzxzldeplem3  49133