Theorem lmodvscl 20833

Description: Closure of scalar product for a left module. (hvmulcl 30940 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 2735	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2735	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2735	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2735	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20820	. . . 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 2108  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  +_gcplusg 17269  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  1_rcur 20139  LModclmod 20815

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-lmod 20817

This theorem is referenced by:  lmodvscld  20834  lmodscaf  20839  lmod0vs  20850  lmodvsmmulgdi  20852  lcomf  20856  lmodvneg1  20860  lmodvsneg  20861  lmodnegadd  20866  lmodsubvs  20873  lmodsubdi  20874  lmodsubdir  20875  lmodvsghm  20878  lmodprop2d  20879  lss1  20893  lssvsubcl  20899  lssvscl  20910  lss1d  20918  lssacs  20922  prdsvscacl  20923  lmodvsinv  20992  lmodvsinv2  20993  islmhm2  20994  0lmhm  20996  idlmhm  20997  lmhmco  20999  lmhmplusg  21000  lmhmvsca  21001  lmhmf1o  21002  lmhmpreima  21004  lmhmeql  21011  pwsdiaglmhm  21013  pwssplit3  21017  lvecvscan  21070  lvecvscan2  21071  lspsnvs  21073  lspfixed  21087  lspexch  21088  lspsolvlem  21101  lspsolv  21102  islbs2  21113  ipass  21603  ipassr  21604  phlssphl  21617  ocvlss  21630  dsmmlss  21702  frlmvscavalb  21728  frlmvplusgscavalb  21729  frlmphl  21739  uvcresum  21751  frlmssuvc2  21753  frlmup1  21756  lindfmm  21785  islindf4  21796  assa2ass  21821  assapropd  21830  asclf  21840  assamulgscmlem1  21857  assamulgscmlem2  21858  mplcoe1  21993  mplmon2cl  22024  mplmon2mul  22025  mplind  22026  ply1tmcl  22207  ply1coe  22234  evl1gsummon  22301  evls1fpws  22305  evls1vsca  22309  asclply1subcl  22310  evls1maplmhm  22313  matvscl  22367  mat0dimscm  22405  matinv  22613  mply1topmatcl  22741  pm2mpmhmlem2  22755  monmat2matmon  22760  chpmat1dlem  22771  chpmat1d  22772  chpdmatlem0  22773  chfacfscmulcl  22793  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmidgsum2  22815  nlmdsdi  24618  nlmdsdir  24619  nlmmul0or  24620  nlmvscnlem2  24622  nlmvscn  24624  clmvscl  25037  cmodscmulexp  25071  cph2ass  25163  ipcau2  25184  tcphcphlem2  25186  tcphcph  25187  cphipval2  25191  4cphipval2  25192  cphipval  25193  pjthlem1  25387  mdegvscale  26030  mdegvsca  26031  plypf1  26167  ttgcontlem1  28810  lmodvslmhm  32990  eqgvscpbl  33311  qusvscpbl  33312  qusvsval  33313  imaslmod  33314  linds2eq  33342  lmhmqusker  33378  ply1degltlss  33552  gsummoncoe1fzo  33553  tngdim  33599  matdim  33601  lindsunlem  33610  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  sitgclbn  34321  lindsadd  37583  lindsenlbs  37585  lfl0  39029  lflsub  39031  lflmul  39032  lfl0f  39033  lfl1  39034  lfladdcl  39035  lflnegcl  39039  lflvscl  39041  lkrlss  39059  eqlkr  39063  lkrlsp  39066  lshpkrlem4  39077  lshpkrlem5  39078  lshpkrlem6  39079  lclkrlem2m  41484  lclkrlem2p  41487  lcdvscl  41570  baerlem3lem1  41672  baerlem5alem1  41673  baerlem5blem1  41674  hdmap14lem1a  41831  hdmap14lem2a  41832  hdmap14lem2N  41834  hdmap14lem3  41835  hdmap14lem4a  41836  hdmap14lem8  41840  hgmapadd  41859  hgmapmul  41860  hgmaprnlem4N  41864  hgmap11  41867  hdmapgln2  41877  hdmapinvlem3  41885  hdmapinvlem4  41886  hdmapglem7b  41893  hlhilphllem  41924  mendassa  43161  ply1mulgsum  48314  lincfsuppcl  48337  linccl  48338  lincvalsng  48340  lincvalpr  48342  lincdifsn  48348  linc1  48349  lincsum  48353  lincscm  48354  lincscmcl  48356  lincext3  48380  lindslinindimp2lem4  48385  lindslinindsimp2  48387  snlindsntor  48395  lincresunit3lem2  48404  lincresunit3  48405  zlmodzxzldeplem3  48426