Theorem lmodvscl 20925

Description: Closure of scalar product for a left module. (hvmulcl 31162 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 571	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 571	. 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 20912	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 498	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1154	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1173	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  +_gcplusg 17269  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  1_rcur 20210  LModclmod 20907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-lmod 20909

This theorem is referenced by:  lmodvscld  20926  lmodscaf  20931  lmod0vs  20942  lmodvsmmulgdi  20944  lcomf  20948  lmodvneg1  20952  lmodvsneg  20953  lmodnegadd  20958  lmodsubvs  20965  lmodsubdi  20966  lmodsubdir  20967  lmodvsghm  20970  lmodprop2d  20971  lss1  20985  lssvsubcl  20991  lssvscl  21002  lss1d  21010  lssacs  21014  prdsvscacl  21015  lmodvsinv  21083  lmodvsinv2  21084  islmhm2  21085  0lmhm  21087  idlmhm  21088  lmhmco  21090  lmhmplusg  21091  lmhmvsca  21092  lmhmf1o  21093  lmhmpreima  21095  lmhmeql  21102  pwsdiaglmhm  21104  pwssplit3  21108  lvecvscan  21161  lvecvscan2  21162  lspsnvs  21164  lspfixed  21178  lspexch  21179  lspsolvlem  21192  lspsolv  21193  islbs2  21204  ipass  21677  ipassr  21678  phlssphl  21691  ocvlss  21704  dsmmlss  21776  frlmvscavalb  21802  frlmvplusgscavalb  21803  frlmphl  21813  uvcresum  21825  frlmssuvc2  21827  frlmup1  21830  lindfmm  21859  islindf4  21870  assa2ass  21895  assapropd  21903  asclf  21913  assamulgscmlem1  21931  assamulgscmlem2  21932  mplcoe1  22070  mplmon2cl  22101  mplmon2mul  22102  mplind  22103  ply1tmcl  22315  ply1coe  22341  evl1gsummon  22408  evls1fpws  22412  evls1vsca  22416  asclply1subcl  22417  evls1maplmhm  22420  matvscl  22471  mat0dimscm  22509  matinv  22717  mply1topmatcl  22845  pm2mpmhmlem2  22859  monmat2matmon  22864  chpmat1dlem  22875  chpmat1d  22876  chpdmatlem0  22877  chfacfscmulcl  22897  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  cpmadugsumfi  22917  cpmidgsum2  22919  nlmdsdi  24721  nlmdsdir  24722  nlmmul0or  24723  nlmvscnlem2  24725  nlmvscn  24727  clmvscl  25130  cmodscmulexp  25164  cph2ass  25255  ipcau2  25276  tcphcphlem2  25278  tcphcph  25279  cphipval2  25283  4cphipval2  25284  cphipval  25285  pjthlem1  25479  mdegvscale  26115  mdegvsca  26116  plypf1  26252  ttgcontlem1  29031  lmodvslmhm  33191  eqgvscpbl  33497  qusvscpbl  33498  qusvsval  33499  imaslmod  33500  linds2eq  33528  lmhmqusker  33564  ply1degltlss  33753  gsummoncoe1fzo  33754  tngdim  33871  matdim  33873  lindsunlem  33882  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  sitgclbn  34601  lindsadd  38076  lindsenlbs  38078  lfl0  39653  lflsub  39655  lflmul  39656  lfl0f  39657  lfl1  39658  lfladdcl  39659  lflnegcl  39663  lflvscl  39665  lkrlss  39683  eqlkr  39687  lkrlsp  39690  lshpkrlem4  39701  lshpkrlem5  39702  lshpkrlem6  39703  lclkrlem2m  42107  lclkrlem2p  42110  lcdvscl  42193  baerlem3lem1  42295  baerlem5alem1  42296  baerlem5blem1  42297  hdmap14lem1a  42454  hdmap14lem2a  42455  hdmap14lem2N  42457  hdmap14lem3  42458  hdmap14lem4a  42459  hdmap14lem8  42463  hgmapadd  42482  hgmapmul  42483  hgmaprnlem4N  42487  hgmap11  42490  hdmapgln2  42500  hdmapinvlem3  42508  hdmapinvlem4  42509  hdmapglem7b  42516  hlhilphllem  42547  mendassa  43731  ply1mulgsum  48976  lincfsuppcl  48999  linccl  49000  lincvalsng  49002  lincvalpr  49004  lincdifsn  49010  linc1  49011  lincsum  49015  lincscm  49016  lincscmcl  49018  lincext3  49042  lindslinindimp2lem4  49047  lindslinindsimp2  49049  snlindsntor  49057  lincresunit3lem2  49066  lincresunit3  49067  zlmodzxzldeplem3  49088