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

Theorem lmodvscl 19580
Description: Closure of scalar product for a left module. (hvmulcl 28717 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 262 . 2 (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2 pm4.24 564 . 2 (𝑅𝐾 ↔ (𝑅𝐾𝑅𝐾))
3 pm4.24 564 . 2 (𝑋𝑉 ↔ (𝑋𝑉𝑋𝑉))
4 lmodvscl.v . . . . 5 𝑉 = (Base‘𝑊)
5 eqid 2818 . . . . 5 (+g𝑊) = (+g𝑊)
6 lmodvscl.s . . . . 5 · = ( ·𝑠𝑊)
7 lmodvscl.f . . . . 5 𝐹 = (Scalar‘𝑊)
8 lmodvscl.k . . . . 5 𝐾 = (Base‘𝐹)
9 eqid 2818 . . . . 5 (+g𝐹) = (+g𝐹)
10 eqid 2818 . . . . 5 (.r𝐹) = (.r𝐹)
11 eqid 2818 . . . . 5 (1r𝐹) = (1r𝐹)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 19568 . . . 4 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
1312simpld 495 . . 3 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))))
1413simp1d 1134 . 2 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1153 1 ((𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  .rcmulr 16554  Scalarcsca 16556   ·𝑠 cvsca 16557  1rcur 19180  LModclmod 19563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-lmod 19565
This theorem is referenced by:  lmodscaf  19585  lmod0vs  19596  lmodvsmmulgdi  19598  lcomf  19602  lmodvneg1  19606  lmodvsneg  19607  lmodnegadd  19612  lmodsubvs  19619  lmodsubdi  19620  lmodsubdir  19621  lmodvsghm  19624  lmodprop2d  19625  lss1  19639  lssvsubcl  19644  lssvscl  19656  lss1d  19664  lssacs  19668  prdsvscacl  19669  lmodvsinv  19737  lmodvsinv2  19738  islmhm2  19739  0lmhm  19741  idlmhm  19742  lmhmco  19744  lmhmplusg  19745  lmhmvsca  19746  lmhmf1o  19747  lmhmpreima  19749  lmhmeql  19756  pwsdiaglmhm  19758  pwssplit3  19762  lvecvscan  19812  lvecvscan2  19813  lspsnvs  19815  lspfixed  19829  lspexch  19830  lspsolvlem  19843  lspsolv  19844  islbs2  19855  assa2ass  20023  assapropd  20029  asclf  20039  ascldimulOLD  20045  assamulgscmlem1  20056  assamulgscmlem2  20057  mplcoe1  20174  mplmon2cl  20208  mplmon2mul  20209  mplind  20210  mhpvscacl  20269  ply1tmcl  20368  ply1coe  20392  evl1gsummon  20456  ipass  20717  ipassr  20718  phlssphl  20731  ocvlss  20744  dsmmlss  20816  frlmvscavalb  20842  frlmvplusgscavalb  20843  frlmphl  20853  uvcresum  20865  frlmssuvc2  20867  frlmup1  20870  lindfmm  20899  islindf4  20910  matvscl  20968  mat0dimscm  21006  matinv  21214  mply1topmatcl  21341  pm2mpmhmlem2  21355  monmat2matmon  21360  chpmat1dlem  21371  chpmat1d  21372  chpdmatlem0  21373  chfacfscmulcl  21393  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  cpmadugsumfi  21413  cpmidgsum2  21415  nlmdsdi  23217  nlmdsdir  23218  nlmmul0or  23219  nlmvscnlem2  23221  nlmvscn  23223  clmvscl  23619  cmodscmulexp  23653  cph2ass  23744  ipcau2  23764  tcphcphlem2  23766  tcphcph  23767  cphipval2  23771  4cphipval2  23772  cphipval  23773  pjthlem1  23967  mdegvscale  24596  mdegvsca  24597  plypf1  24729  ttgcontlem1  26598  lmodvslmhm  30615  eqgvscpbl  30846  qusvscpbl  30847  qusscaval  30848  imaslmod  30849  linds2eq  30868  tngdim  30910  matdim  30912  lindsunlem  30919  lbsdiflsp0  30921  fedgmullem1  30924  fedgmullem2  30925  sitgclbn  31500  lindsadd  34766  lindsenlbs  34768  lfl0  36081  lflsub  36083  lflmul  36084  lfl0f  36085  lfl1  36086  lfladdcl  36087  lflnegcl  36091  lflvscl  36093  lkrlss  36111  eqlkr  36115  lkrlsp  36118  lshpkrlem4  36129  lshpkrlem5  36130  lshpkrlem6  36131  lclkrlem2m  38535  lclkrlem2p  38538  lcdvscl  38621  baerlem3lem1  38723  baerlem5alem1  38724  baerlem5blem1  38725  hdmap14lem1a  38882  hdmap14lem2a  38883  hdmap14lem2N  38885  hdmap14lem3  38886  hdmap14lem4a  38887  hdmap14lem8  38891  hgmapadd  38910  hgmapmul  38911  hgmaprnlem4N  38915  hgmap11  38918  hdmapgln2  38928  hdmapinvlem3  38936  hdmapinvlem4  38937  hdmapglem7b  38944  hlhilphllem  38975  frlmsnic  39027  prjspvs  39138  prjspeclsp  39140  mendassa  39672  ply1mulgsum  44372  lincfsuppcl  44396  linccl  44397  lincvalsng  44399  lincvalpr  44401  lincdifsn  44407  linc1  44408  lincsum  44412  lincscm  44413  lincscmcl  44415  lincext3  44439  lindslinindimp2lem4  44444  lindslinindsimp2  44446  snlindsntor  44454  lincresunit3lem2  44463  lincresunit3  44464  zlmodzxzldeplem3  44485
  Copyright terms: Public domain W3C validator