Theorem lmodvscl 20873

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  1_rcur 20162  LModclmod 20855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-lmod 20857

This theorem is referenced by:  lmodvscld  20874  lmodscaf  20879  lmod0vs  20890  lmodvsmmulgdi  20892  lcomf  20896  lmodvneg1  20900  lmodvsneg  20901  lmodnegadd  20906  lmodsubvs  20913  lmodsubdi  20914  lmodsubdir  20915  lmodvsghm  20918  lmodprop2d  20919  lss1  20933  lssvsubcl  20939  lssvscl  20950  lss1d  20958  lssacs  20962  prdsvscacl  20963  lmodvsinv  21031  lmodvsinv2  21032  islmhm2  21033  0lmhm  21035  idlmhm  21036  lmhmco  21038  lmhmplusg  21039  lmhmvsca  21040  lmhmf1o  21041  lmhmpreima  21043  lmhmeql  21050  pwsdiaglmhm  21052  pwssplit3  21056  lvecvscan  21109  lvecvscan2  21110  lspsnvs  21112  lspfixed  21126  lspexch  21127  lspsolvlem  21140  lspsolv  21141  islbs2  21152  ipass  21625  ipassr  21626  phlssphl  21639  ocvlss  21652  dsmmlss  21724  frlmvscavalb  21750  frlmvplusgscavalb  21751  frlmphl  21761  uvcresum  21773  frlmssuvc2  21775  frlmup1  21778  lindfmm  21807  islindf4  21818  assa2ass  21843  assapropd  21851  asclf  21861  assamulgscmlem1  21879  assamulgscmlem2  21880  mplcoe1  22015  mplmon2cl  22046  mplmon2mul  22047  mplind  22048  ply1tmcl  22237  ply1coe  22263  evl1gsummon  22330  evls1fpws  22334  evls1vsca  22338  asclply1subcl  22339  evls1maplmhm  22342  matvscl  22396  mat0dimscm  22434  matinv  22642  mply1topmatcl  22770  pm2mpmhmlem2  22784  monmat2matmon  22789  chpmat1dlem  22800  chpmat1d  22801  chpdmatlem0  22802  chfacfscmulcl  22822  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmidgsum2  22844  nlmdsdi  24646  nlmdsdir  24647  nlmmul0or  24648  nlmvscnlem2  24650  nlmvscn  24652  clmvscl  25055  cmodscmulexp  25089  cph2ass  25180  ipcau2  25201  tcphcphlem2  25203  tcphcph  25204  cphipval2  25208  4cphipval2  25209  cphipval  25210  pjthlem1  25404  mdegvscale  26040  mdegvsca  26041  plypf1  26177  ttgcontlem1  28953  lmodvslmhm  33111  eqgvscpbl  33410  qusvscpbl  33411  qusvsval  33412  imaslmod  33413  linds2eq  33441  lmhmqusker  33477  ply1degltlss  33656  gsummoncoe1fzo  33657  tngdim  33757  matdim  33759  lindsunlem  33768  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  sitgclbn  34487  lindsadd  37934  lindsenlbs  37936  lfl0  39511  lflsub  39513  lflmul  39514  lfl0f  39515  lfl1  39516  lfladdcl  39517  lflnegcl  39521  lflvscl  39523  lkrlss  39541  eqlkr  39545  lkrlsp  39548  lshpkrlem4  39559  lshpkrlem5  39560  lshpkrlem6  39561  lclkrlem2m  41965  lclkrlem2p  41968  lcdvscl  42051  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  hdmap14lem1a  42312  hdmap14lem2a  42313  hdmap14lem2N  42315  hdmap14lem3  42316  hdmap14lem4a  42317  hdmap14lem8  42321  hgmapadd  42340  hgmapmul  42341  hgmaprnlem4N  42345  hgmap11  42348  hdmapgln2  42358  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem7b  42374  hlhilphllem  42405  mendassa  43618  ply1mulgsum  48866  lincfsuppcl  48889  linccl  48890  lincvalsng  48892  lincvalpr  48894  lincdifsn  48900  linc1  48901  lincsum  48905  lincscm  48906  lincscmcl  48908  lincext3  48932  lindslinindimp2lem4  48937  lindslinindsimp2  48939  snlindsntor  48947  lincresunit3lem2  48956  lincresunit3  48957  zlmodzxzldeplem3  48978