Theorem lmodvscl 20864

Description: Closure of scalar product for a left module. (hvmulcl 31099 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 2737	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2737	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2737	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2737	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20851	. . . 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 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Scalarcsca 17214   ·_𝑠 cvsca 17215  1_rcur 20153  LModclmod 20846

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-lmod 20848

This theorem is referenced by:  lmodvscld  20865  lmodscaf  20870  lmod0vs  20881  lmodvsmmulgdi  20883  lcomf  20887  lmodvneg1  20891  lmodvsneg  20892  lmodnegadd  20897  lmodsubvs  20904  lmodsubdi  20905  lmodsubdir  20906  lmodvsghm  20909  lmodprop2d  20910  lss1  20924  lssvsubcl  20930  lssvscl  20941  lss1d  20949  lssacs  20953  prdsvscacl  20954  lmodvsinv  21023  lmodvsinv2  21024  islmhm2  21025  0lmhm  21027  idlmhm  21028  lmhmco  21030  lmhmplusg  21031  lmhmvsca  21032  lmhmf1o  21033  lmhmpreima  21035  lmhmeql  21042  pwsdiaglmhm  21044  pwssplit3  21048  lvecvscan  21101  lvecvscan2  21102  lspsnvs  21104  lspfixed  21118  lspexch  21119  lspsolvlem  21132  lspsolv  21133  islbs2  21144  ipass  21635  ipassr  21636  phlssphl  21649  ocvlss  21662  dsmmlss  21734  frlmvscavalb  21760  frlmvplusgscavalb  21761  frlmphl  21771  uvcresum  21783  frlmssuvc2  21785  frlmup1  21788  lindfmm  21817  islindf4  21828  assa2ass  21853  assapropd  21861  asclf  21871  assamulgscmlem1  21889  assamulgscmlem2  21890  mplcoe1  22025  mplmon2cl  22056  mplmon2mul  22057  mplind  22058  ply1tmcl  22247  ply1coe  22273  evl1gsummon  22340  evls1fpws  22344  evls1vsca  22348  asclply1subcl  22349  evls1maplmhm  22352  matvscl  22406  mat0dimscm  22444  matinv  22652  mply1topmatcl  22780  pm2mpmhmlem2  22794  monmat2matmon  22799  chpmat1dlem  22810  chpmat1d  22811  chpdmatlem0  22812  chfacfscmulcl  22832  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmidgsum2  22854  nlmdsdi  24656  nlmdsdir  24657  nlmmul0or  24658  nlmvscnlem2  24660  nlmvscn  24662  clmvscl  25065  cmodscmulexp  25099  cph2ass  25190  ipcau2  25211  tcphcphlem2  25213  tcphcph  25214  cphipval2  25218  4cphipval2  25219  cphipval  25220  pjthlem1  25414  mdegvscale  26050  mdegvsca  26051  plypf1  26187  ttgcontlem1  28967  lmodvslmhm  33126  eqgvscpbl  33425  qusvscpbl  33426  qusvsval  33427  imaslmod  33428  linds2eq  33456  lmhmqusker  33492  ply1degltlss  33671  gsummoncoe1fzo  33672  tngdim  33773  matdim  33775  lindsunlem  33784  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  sitgclbn  34503  lindsadd  37948  lindsenlbs  37950  lfl0  39525  lflsub  39527  lflmul  39528  lfl0f  39529  lfl1  39530  lfladdcl  39531  lflnegcl  39535  lflvscl  39537  lkrlss  39555  eqlkr  39559  lkrlsp  39562  lshpkrlem4  39573  lshpkrlem5  39574  lshpkrlem6  39575  lclkrlem2m  41979  lclkrlem2p  41982  lcdvscl  42065  baerlem3lem1  42167  baerlem5alem1  42168  baerlem5blem1  42169  hdmap14lem1a  42326  hdmap14lem2a  42327  hdmap14lem2N  42329  hdmap14lem3  42330  hdmap14lem4a  42331  hdmap14lem8  42335  hgmapadd  42354  hgmapmul  42355  hgmaprnlem4N  42359  hgmap11  42362  hdmapgln2  42372  hdmapinvlem3  42380  hdmapinvlem4  42381  hdmapglem7b  42388  hlhilphllem  42419  mendassa  43636  ply1mulgsum  48878  lincfsuppcl  48901  linccl  48902  lincvalsng  48904  lincvalpr  48906  lincdifsn  48912  linc1  48913  lincsum  48917  lincscm  48918  lincscmcl  48920  lincext3  48944  lindslinindimp2lem4  48949  lindslinindsimp2  48951  snlindsntor  48959  lincresunit3lem2  48968  lincresunit3  48969  zlmodzxzldeplem3  48990