MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvscl Structured version   Visualization version   GIF version

Theorem lmodvscl 18928
Description: Closure of scalar product for a left module. (hvmulcl 27998 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
StepHypRef Expression
1 biid 251 . 2 (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2 pm4.24 676 . 2 (𝑅𝐾 ↔ (𝑅𝐾𝑅𝐾))
3 pm4.24 676 . 2 (𝑋𝑉 ↔ (𝑋𝑉𝑋𝑉))
4 lmodvscl.v . . . . 5 𝑉 = (Base‘𝑊)
5 eqid 2651 . . . . 5 (+g𝑊) = (+g𝑊)
6 lmodvscl.s . . . . 5 · = ( ·𝑠𝑊)
7 lmodvscl.f . . . . 5 𝐹 = (Scalar‘𝑊)
8 lmodvscl.k . . . . 5 𝐾 = (Base‘𝐹)
9 eqid 2651 . . . . 5 (+g𝐹) = (+g𝐹)
10 eqid 2651 . . . . 5 (.r𝐹) = (.r𝐹)
11 eqid 2651 . . . . 5 (1r𝐹) = (1r𝐹)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 18916 . . . 4 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
1312simpld 474 . . 3 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))))
1413simp1d 1093 . 2 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1409 1 ((𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  cfv 5926  (class class class)co 6690  Basecbs 15904  +gcplusg 15988  .rcmulr 15989  Scalarcsca 15991   ·𝑠 cvsca 15992  1rcur 18547  LModclmod 18911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-lmod 18913
This theorem is referenced by:  lmodscaf  18933  lmod0vs  18944  lmodvsmmulgdi  18946  lcomf  18950  lmodvneg1  18954  lmodvsneg  18955  lmodnegadd  18960  lmodsubvs  18967  lmodsubdi  18968  lmodsubdir  18969  lmodvsghm  18972  lmodprop2d  18973  lss1  18987  lssvsubcl  18992  lssvscl  19003  lss1d  19011  lssacs  19015  prdsvscacl  19016  lmodvsinv  19084  lmodvsinv2  19085  islmhm2  19086  0lmhm  19088  idlmhm  19089  lmhmco  19091  lmhmplusg  19092  lmhmvsca  19093  lmhmf1o  19094  lmhmpreima  19096  lmhmeql  19103  pwsdiaglmhm  19105  pwssplit3  19109  lvecvscan  19159  lvecvscan2  19160  lspsnvs  19162  lspfixed  19176  lspexch  19177  lspsolvlem  19190  lspsolv  19191  islbs2  19202  assa2ass  19370  assapropd  19375  asclf  19385  asclrhm  19390  assamulgscmlem1  19396  assamulgscmlem2  19397  mplcoe1  19513  mplmon2cl  19548  mplmon2mul  19549  mplind  19550  ply1tmcl  19690  ply1coe  19714  evl1gsummon  19777  ipass  20038  ipassr  20039  ocvlss  20064  dsmmlss  20136  frlmphl  20168  uvcresum  20180  frlmssuvc2  20182  frlmup1  20185  lindfmm  20214  islindf4  20225  matvscl  20285  mat0dimscm  20323  matinv  20531  mply1topmatcl  20658  pm2mpmhmlem2  20672  monmat2matmon  20677  chpmat1dlem  20688  chpmat1d  20689  chpdmatlem0  20690  chfacfscmulcl  20710  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadugsumfi  20730  cpmidgsum2  20732  nlmdsdi  22532  nlmdsdir  22533  nlmmul0or  22534  nlmvscnlem2  22536  nlmvscn  22538  clmvscl  22934  cmodscmulexp  22968  cph2ass  23059  ipcau2  23079  tchcphlem2  23081  tchcph  23082  cphipval2  23086  4cphipval2  23087  cphipval  23088  pjthlem1  23254  mdegvscale  23880  mdegvsca  23881  plypf1  24013  ttgcontlem1  25810  sitgclbn  30533  lindsenlbs  33534  lfl0  34670  lflsub  34672  lflmul  34673  lfl0f  34674  lfl1  34675  lfladdcl  34676  lflnegcl  34680  lflvscl  34682  lkrlss  34700  eqlkr  34704  lkrlsp  34707  lshpkrlem4  34718  lshpkrlem5  34719  lshpkrlem6  34720  lclkrlem2m  37125  lclkrlem2p  37128  lcdvscl  37211  baerlem3lem1  37313  baerlem5alem1  37314  baerlem5blem1  37315  hdmap14lem1a  37475  hdmap14lem2a  37476  hdmap14lem2N  37478  hdmap14lem3  37479  hdmap14lem4a  37480  hdmap14lem8  37484  hgmapadd  37503  hgmapmul  37504  hgmaprnlem4N  37508  hgmap11  37511  hdmapgln2  37521  hdmapinvlem3  37529  hdmapinvlem4  37530  hdmapglem7b  37537  hlhilphllem  37568  mendassa  38081  ply1mulgsum  42503  lincfsuppcl  42527  linccl  42528  lincvalsng  42530  lincvalpr  42532  lincdifsn  42538  linc1  42539  lincsum  42543  lincscm  42544  lincscmcl  42546  lincext3  42570  lindslinindimp2lem4  42575  lindslinindsimp2  42577  snlindsntor  42585  lincresunit3lem2  42594  lincresunit3  42595  zlmodzxzldeplem3  42616
  Copyright terms: Public domain W3C validator