Theorem lmodvscl 21133

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  ._rcmulr 17409  Scalarcsca 17411   ·_𝑠 cvsca 17412  1_rcur 20387  LModclmod 21115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-lmod 21117

This theorem is used by:  lmodvscld  21134  lmodscaf  21139  lmod0vs  21150  lmodvsmmulgdi  21152  lcomf  21156  lmodvneg1  21160  lmodvsneg  21161  lmodnegadd  21166  lmodsubvs  21173  lmodsubdi  21174  lmodsubdir  21175  lmodvsghm  21178  lmodprop2d  21179  lss1  21193  lssvsubcl  21199  lssvscl  21210  lss1d  21218  lssacs  21222  prdsvscacl  21223  lmodvsinv  21291  lmodvsinv2  21292  islmhm2  21293  0lmhm  21295  idlmhm  21296  lmhmco  21298  lmhmplusg  21299  lmhmvsca  21300  lmhmf1o  21301  lmhmpreima  21303  lmhmeql  21310  pwsdiaglmhm  21312  pwssplit3  21316  lvecvscan  21369  lvecvscan2  21370  lspsnvs  21372  lspfixed  21386  lspexch  21387  lspsolvlem  21400  lspsolv  21401  islbs2  21412  ipass  21931  ipassr  21932  phlssphl  21945  ocvlss  21958  dsmmlss  22030  frlmvscavalb  22056  frlmvplusgscavalb  22057  frlmphl  22067  uvcresum  22079  frlmssuvc2  22081  frlmup1  22084  lindfmm  22113  islindf4  22124  lindsenlbs  22137  assa2ass  22151  assapropd  22159  asclf  22169  assamulgscmlem1  22187  assamulgscmlem2  22188  mplcoe1  22326  mplmon2cl  22357  mplmon2mul  22358  mplind  22359  ply1tmcl  22571  ply1coe  22596  evl1gsummon  22663  evls1fpws  22667  evls1vsca  22671  asclply1subcl  22672  evls1maplmhm  22675  matvscl  22726  mat0dimscm  22764  matinv  22972  mply1topmatcl  23103  pm2mpmhmlem2  23117  monmat2matmon  23122  chpmat1dlem  23133  chpmat1d  23134  chpdmatlem0  23135  chfacfscmulcl  23155  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  cpmadugsumfi  23175  cpmidgsum2  23177  nlmdsdi  24980  nlmdsdir  24981  nlmmul0or  24982  nlmvscnlem2  24984  nlmvscn  24986  clmvscl  25389  cmodscmulexp  25423  cph2ass  25514  ipcau2  25535  tcphcphlem2  25537  tcphcph  25538  cphipval2  25542  4cphipval2  25543  cphipval  25544  pjthlem1  25738  mdegvscale  26373  mdegvsca  26374  plypf1  26511  ttgcontlem1  29444  lmodvslmhm  33593  eqgvscpbl  33893  qusvscpbl  33894  qusvsval  33895  imaslmod  33896  linds2eq  33918  lmhmqusker  33950  ply1degltlss  34110  gsummoncoe1fzo  34111  tngdim  34227  matdim  34229  lindsunlem  34238  lbsdiflsp0  34240  fedgmullem1  34243  fedgmullem2  34244  sitgclbn  34958  lindsadd  38504  lfl0  40090  lflsub  40092  lflmul  40093  lfl0f  40094  lfl1  40095  lfladdcl  40096  lflnegcl  40100  lflvscl  40102  lkrlss  40120  eqlkr  40124  lkrlsp  40127  lshpkrlem4  40138  lshpkrlem5  40139  lshpkrlem6  40140  lclkrlem2m  42544  lclkrlem2p  42547  lcdvscl  42630  baerlem3lem1  42732  baerlem5alem1  42733  baerlem5blem1  42734  hdmap14lem1a  42891  hdmap14lem2a  42892  hdmap14lem2N  42894  hdmap14lem3  42895  hdmap14lem4a  42896  hdmap14lem8  42900  hgmapadd  42919  hgmapmul  42920  hgmaprnlem4N  42924  hgmap11  42927  hdmapgln2  42937  hdmapinvlem3  42945  hdmapinvlem4  42946  hdmapglem7b  42953  hlhilphllem  42984  mendassa  44150  ply1mulgsum  49446  lincfsuppcl  49469  linccl  49470  lincvalsng  49472  lincvalpr  49474  lincdifsn  49480  linc1  49481  lincsum  49485  lincscm  49486  lincscmcl  49488  lincext3  49512  lindslinindimp2lem4  49517  lindslinindsimp2  49519  snlindsntor  49527  lincresunit3lem2  49536  lincresunit3  49537  zlmodzxzldeplem3  49558