Theorem lmodvscl 21183

Description: Closure of scalar product for a left module. (hvmulcl 31645 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 2763	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2763	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2763	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2763	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 21170	. . . 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 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  ._rcmulr 17458  Scalarcsca 17460   ·_𝑠 cvsca 17461  1_rcur 20437  LModclmod 21165

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-lmod 21167

This theorem is used by:  lmodvscld  21184  lmodscaf  21189  lmod0vs  21200  lmodvsmmulgdi  21202  lcomf  21206  lmodvneg1  21210  lmodvsneg  21211  lmodnegadd  21216  lmodsubvs  21223  lmodsubdi  21224  lmodsubdir  21225  lmodvsghm  21228  lmodprop2d  21229  lss1  21243  lssvsubcl  21249  lssvscl  21260  lss1d  21268  lssacs  21272  prdsvscacl  21273  lmodvsinv  21341  lmodvsinv2  21342  islmhm2  21343  0lmhm  21345  idlmhm  21346  lmhmco  21348  lmhmplusg  21349  lmhmvsca  21350  lmhmf1o  21351  lmhmpreima  21353  lmhmeql  21360  pwsdiaglmhm  21362  pwssplit3  21366  lvecvscan  21419  lvecvscan2  21420  lspsnvs  21422  lspfixed  21436  lspexch  21437  lspsolvlem  21450  lspsolv  21451  islbs2  21462  ipass  21981  ipassr  21982  phlssphl  21995  ocvlss  22008  dsmmlss  22080  frlmvscavalb  22106  frlmvplusgscavalb  22107  frlmphl  22117  uvcresum  22129  frlmssuvc2  22131  frlmup1  22134  lindfmm  22163  islindf4  22174  lindsenlbs  22187  assa2ass  22201  assapropd  22209  asclf  22219  assamulgscmlem1  22237  assamulgscmlem2  22238  mplcoe1  22376  mplmon2cl  22407  mplmon2mul  22408  mplind  22409  ply1tmcl  22621  ply1coe  22646  evl1gsummon  22713  evls1fpws  22717  evls1vsca  22721  asclply1subcl  22722  evls1maplmhm  22725  matvscl  22776  mat0dimscm  22814  matinv  23022  mply1topmatcl  23153  pm2mpmhmlem2  23167  monmat2matmon  23172  chpmat1dlem  23183  chpmat1d  23184  chpdmatlem0  23185  chfacfscmulcl  23205  cpmadugsumlemB  23222  cpmadugsumlemC  23223  cpmadugsumlemF  23224  cpmadugsumfi  23225  cpmidgsum2  23227  nlmdsdi  25030  nlmdsdir  25031  nlmmul0or  25032  nlmvscnlem2  25034  nlmvscn  25036  clmvscl  25439  cmodscmulexp  25473  cph2ass  25564  ipcau2  25585  tcphcphlem2  25587  tcphcph  25588  cphipval2  25592  4cphipval2  25593  cphipval  25594  pjthlem1  25788  mdegvscale  26423  mdegvsca  26424  plypf1  26561  ttgcontlem1  29492  lmodvslmhm  33681  eqgvscpbl  33981  qusvscpbl  33982  qusvsval  33983  imaslmod  33984  linds2eq  34006  lmhmqusker  34038  ply1degltlss  34198  gsummoncoe1fzo  34199  tngdim  34315  matdim  34317  lindsunlem  34326  lbsdiflsp0  34328  fedgmullem1  34331  fedgmullem2  34332  sitgclbn  35045  lindsadd  38728  lfl0  40314  lflsub  40316  lflmul  40317  lfl0f  40318  lfl1  40319  lfladdcl  40320  lflnegcl  40324  lflvscl  40326  lkrlss  40344  eqlkr  40348  lkrlsp  40351  lshpkrlem4  40362  lshpkrlem5  40363  lshpkrlem6  40364  lclkrlem2m  42768  lclkrlem2p  42771  lcdvscl  42854  baerlem3lem1  42956  baerlem5alem1  42957  baerlem5blem1  42958  hdmap14lem1a  43115  hdmap14lem2a  43116  hdmap14lem2N  43118  hdmap14lem3  43119  hdmap14lem4a  43120  hdmap14lem8  43124  hgmapadd  43143  hgmapmul  43144  hgmaprnlem4N  43148  hgmap11  43151  hdmapgln2  43161  hdmapinvlem3  43169  hdmapinvlem4  43170  hdmapglem7b  43177  hlhilphllem  43208  mendassa  44384  ply1mulgsum  49707  lincfsuppcl  49730  linccl  49731  lincvalsng  49733  lincvalpr  49735  lincdifsn  49741  linc1  49742  lincsum  49746  lincscm  49747  lincscmcl  49749  lincext3  49773  lindslinindimp2lem4  49778  lindslinindsimp2  49780  snlindsntor  49788  lincresunit3lem2  49797  lincresunit3  49798  zlmodzxzldeplem3  49819