Theorem lmodvscl 20791

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  1_rcur 20097  LModclmod 20773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-lmod 20775

This theorem is referenced by:  lmodvscld  20792  lmodscaf  20797  lmod0vs  20808  lmodvsmmulgdi  20810  lcomf  20814  lmodvneg1  20818  lmodvsneg  20819  lmodnegadd  20824  lmodsubvs  20831  lmodsubdi  20832  lmodsubdir  20833  lmodvsghm  20836  lmodprop2d  20837  lss1  20851  lssvsubcl  20857  lssvscl  20868  lss1d  20876  lssacs  20880  prdsvscacl  20881  lmodvsinv  20950  lmodvsinv2  20951  islmhm2  20952  0lmhm  20954  idlmhm  20955  lmhmco  20957  lmhmplusg  20958  lmhmvsca  20959  lmhmf1o  20960  lmhmpreima  20962  lmhmeql  20969  pwsdiaglmhm  20971  pwssplit3  20975  lvecvscan  21028  lvecvscan2  21029  lspsnvs  21031  lspfixed  21045  lspexch  21046  lspsolvlem  21059  lspsolv  21060  islbs2  21071  ipass  21561  ipassr  21562  phlssphl  21575  ocvlss  21588  dsmmlss  21660  frlmvscavalb  21686  frlmvplusgscavalb  21687  frlmphl  21697  uvcresum  21709  frlmssuvc2  21711  frlmup1  21714  lindfmm  21743  islindf4  21754  assa2ass  21779  assapropd  21788  asclf  21798  assamulgscmlem1  21815  assamulgscmlem2  21816  mplcoe1  21951  mplmon2cl  21982  mplmon2mul  21983  mplind  21984  ply1tmcl  22165  ply1coe  22192  evl1gsummon  22259  evls1fpws  22263  evls1vsca  22267  asclply1subcl  22268  evls1maplmhm  22271  matvscl  22325  mat0dimscm  22363  matinv  22571  mply1topmatcl  22699  pm2mpmhmlem2  22713  monmat2matmon  22718  chpmat1dlem  22729  chpmat1d  22730  chpdmatlem0  22731  chfacfscmulcl  22751  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  cpmadugsumfi  22771  cpmidgsum2  22773  nlmdsdi  24576  nlmdsdir  24577  nlmmul0or  24578  nlmvscnlem2  24580  nlmvscn  24582  clmvscl  24995  cmodscmulexp  25029  cph2ass  25120  ipcau2  25141  tcphcphlem2  25143  tcphcph  25144  cphipval2  25148  4cphipval2  25149  cphipval  25150  pjthlem1  25344  mdegvscale  25987  mdegvsca  25988  plypf1  26124  ttgcontlem1  28819  lmodvslmhm  32997  eqgvscpbl  33328  qusvscpbl  33329  qusvsval  33330  imaslmod  33331  linds2eq  33359  lmhmqusker  33395  ply1degltlss  33569  gsummoncoe1fzo  33570  tngdim  33616  matdim  33618  lindsunlem  33627  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  sitgclbn  34341  lindsadd  37614  lindsenlbs  37616  lfl0  39065  lflsub  39067  lflmul  39068  lfl0f  39069  lfl1  39070  lfladdcl  39071  lflnegcl  39075  lflvscl  39077  lkrlss  39095  eqlkr  39099  lkrlsp  39102  lshpkrlem4  39113  lshpkrlem5  39114  lshpkrlem6  39115  lclkrlem2m  41520  lclkrlem2p  41523  lcdvscl  41606  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  hdmap14lem1a  41867  hdmap14lem2a  41868  hdmap14lem2N  41870  hdmap14lem3  41871  hdmap14lem4a  41872  hdmap14lem8  41876  hgmapadd  41895  hgmapmul  41896  hgmaprnlem4N  41900  hgmap11  41903  hdmapgln2  41913  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem7b  41929  hlhilphllem  41960  mendassa  43186  ply1mulgsum  48383  lincfsuppcl  48406  linccl  48407  lincvalsng  48409  lincvalpr  48411  lincdifsn  48417  linc1  48418  lincsum  48422  lincscm  48423  lincscmcl  48425  lincext3  48449  lindslinindimp2lem4  48454  lindslinindsimp2  48456  snlindsntor  48464  lincresunit3lem2  48473  lincresunit3  48474  zlmodzxzldeplem3  48495