Theorem lmodvscl 20841

Description: Closure of scalar product for a left module. (hvmulcl 31100 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 20828	. . . 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 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  1_rcur 20128  LModclmod 20823

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 5253

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-lmod 20825

This theorem is referenced by:  lmodvscld  20842  lmodscaf  20847  lmod0vs  20858  lmodvsmmulgdi  20860  lcomf  20864  lmodvneg1  20868  lmodvsneg  20869  lmodnegadd  20874  lmodsubvs  20881  lmodsubdi  20882  lmodsubdir  20883  lmodvsghm  20886  lmodprop2d  20887  lss1  20901  lssvsubcl  20907  lssvscl  20918  lss1d  20926  lssacs  20930  prdsvscacl  20931  lmodvsinv  21000  lmodvsinv2  21001  islmhm2  21002  0lmhm  21004  idlmhm  21005  lmhmco  21007  lmhmplusg  21008  lmhmvsca  21009  lmhmf1o  21010  lmhmpreima  21012  lmhmeql  21019  pwsdiaglmhm  21021  pwssplit3  21025  lvecvscan  21078  lvecvscan2  21079  lspsnvs  21081  lspfixed  21095  lspexch  21096  lspsolvlem  21109  lspsolv  21110  islbs2  21121  ipass  21612  ipassr  21613  phlssphl  21626  ocvlss  21639  dsmmlss  21711  frlmvscavalb  21737  frlmvplusgscavalb  21738  frlmphl  21748  uvcresum  21760  frlmssuvc2  21762  frlmup1  21765  lindfmm  21794  islindf4  21805  assa2ass  21830  assapropd  21839  asclf  21849  assamulgscmlem1  21867  assamulgscmlem2  21868  mplcoe1  22004  mplmon2cl  22035  mplmon2mul  22036  mplind  22037  ply1tmcl  22226  ply1coe  22254  evl1gsummon  22321  evls1fpws  22325  evls1vsca  22329  asclply1subcl  22330  evls1maplmhm  22333  matvscl  22387  mat0dimscm  22425  matinv  22633  mply1topmatcl  22761  pm2mpmhmlem2  22775  monmat2matmon  22780  chpmat1dlem  22791  chpmat1d  22792  chpdmatlem0  22793  chfacfscmulcl  22813  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmidgsum2  22835  nlmdsdi  24637  nlmdsdir  24638  nlmmul0or  24639  nlmvscnlem2  24641  nlmvscn  24643  clmvscl  25056  cmodscmulexp  25090  cph2ass  25181  ipcau2  25202  tcphcphlem2  25204  tcphcph  25205  cphipval2  25209  4cphipval2  25210  cphipval  25211  pjthlem1  25405  mdegvscale  26048  mdegvsca  26049  plypf1  26185  ttgcontlem1  28969  lmodvslmhm  33143  eqgvscpbl  33442  qusvscpbl  33443  qusvsval  33444  imaslmod  33445  linds2eq  33473  lmhmqusker  33509  ply1degltlss  33688  gsummoncoe1fzo  33689  tngdim  33790  matdim  33792  lindsunlem  33801  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  sitgclbn  34520  lindsadd  37858  lindsenlbs  37860  lfl0  39435  lflsub  39437  lflmul  39438  lfl0f  39439  lfl1  39440  lfladdcl  39441  lflnegcl  39445  lflvscl  39447  lkrlss  39465  eqlkr  39469  lkrlsp  39472  lshpkrlem4  39483  lshpkrlem5  39484  lshpkrlem6  39485  lclkrlem2m  41889  lclkrlem2p  41892  lcdvscl  41975  baerlem3lem1  42077  baerlem5alem1  42078  baerlem5blem1  42079  hdmap14lem1a  42236  hdmap14lem2a  42237  hdmap14lem2N  42239  hdmap14lem3  42240  hdmap14lem4a  42241  hdmap14lem8  42245  hgmapadd  42264  hgmapmul  42265  hgmaprnlem4N  42269  hgmap11  42272  hdmapgln2  42282  hdmapinvlem3  42290  hdmapinvlem4  42291  hdmapglem7b  42298  hlhilphllem  42329  mendassa  43541  ply1mulgsum  48744  lincfsuppcl  48767  linccl  48768  lincvalsng  48770  lincvalpr  48772  lincdifsn  48778  linc1  48779  lincsum  48783  lincscm  48784  lincscmcl  48786  lincext3  48810  lindslinindimp2lem4  48815  lindslinindsimp2  48817  snlindsntor  48825  lincresunit3lem2  48834  lincresunit3  48835  zlmodzxzldeplem3  48856