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

Theorem lmodvscl 19091
Description: Closure of scalar product for a left module. (hvmulcl 28208 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 252 . 2 (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2 pm4.24 555 . 2 (𝑅𝐾 ↔ (𝑅𝐾𝑅𝐾))
3 pm4.24 555 . 2 (𝑋𝑉 ↔ (𝑋𝑉𝑋𝑉))
4 lmodvscl.v . . . . 5 𝑉 = (Base‘𝑊)
5 eqid 2817 . . . . 5 (+g𝑊) = (+g𝑊)
6 lmodvscl.s . . . . 5 · = ( ·𝑠𝑊)
7 lmodvscl.f . . . . 5 𝐹 = (Scalar‘𝑊)
8 lmodvscl.k . . . . 5 𝐾 = (Base‘𝐹)
9 eqid 2817 . . . . 5 (+g𝐹) = (+g𝐹)
10 eqid 2817 . . . . 5 (.r𝐹) = (.r𝐹)
11 eqid 2817 . . . . 5 (1r𝐹) = (1r𝐹)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 19079 . . . 4 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
1312simpld 484 . . 3 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))))
1413simp1d 1165 . 2 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1193 1 ((𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2157  cfv 6108  (class class class)co 6881  Basecbs 16075  +gcplusg 16160  .rcmulr 16161  Scalarcsca 16163   ·𝑠 cvsca 16164  1rcur 18710  LModclmod 19074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-nul 4994
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6071  df-fv 6116  df-ov 6884  df-lmod 19076
This theorem is referenced by:  lmodscaf  19096  lmod0vs  19107  lmodvsmmulgdi  19109  lcomf  19113  lmodvneg1  19117  lmodvsneg  19118  lmodnegadd  19123  lmodsubvs  19130  lmodsubdi  19131  lmodsubdir  19132  lmodvsghm  19135  lmodprop2d  19136  lss1  19150  lssvsubcl  19155  lssvscl  19169  lss1d  19177  lssacs  19181  prdsvscacl  19182  lmodvsinv  19250  lmodvsinv2  19251  islmhm2  19252  0lmhm  19254  idlmhm  19255  lmhmco  19257  lmhmplusg  19258  lmhmvsca  19259  lmhmf1o  19260  lmhmpreima  19262  lmhmeql  19269  pwsdiaglmhm  19271  pwssplit3  19275  lvecvscan  19325  lvecvscan2  19326  lspsnvs  19328  lspfixed  19342  lspfixedOLD  19343  lspexch  19344  lspsolvlem  19357  lspsolv  19358  islbs2  19370  assa2ass  19538  assapropd  19543  asclf  19553  asclrhm  19558  assamulgscmlem1  19564  assamulgscmlem2  19565  mplcoe1  19681  mplmon2cl  19715  mplmon2mul  19716  mplind  19717  ply1tmcl  19857  ply1coe  19881  evl1gsummon  19944  ipass  20207  ipassr  20208  phlssphl  20221  ocvlss  20234  dsmmlss  20306  frlmphl  20338  uvcresum  20350  frlmssuvc2  20352  frlmup1  20355  lindfmm  20384  islindf4  20395  matvscl  20455  mat0dimscm  20494  matinv  20703  mply1topmatcl  20831  pm2mpmhmlem2  20845  monmat2matmon  20850  chpmat1dlem  20861  chpmat1d  20862  chpdmatlem0  20863  chfacfscmulcl  20883  cpmadugsumlemB  20900  cpmadugsumlemC  20901  cpmadugsumlemF  20902  cpmadugsumfi  20903  cpmidgsum2  20905  nlmdsdi  22706  nlmdsdir  22707  nlmmul0or  22708  nlmvscnlem2  22710  nlmvscn  22712  clmvscl  23108  cmodscmulexp  23142  cph2ass  23233  ipcau2  23253  tchcphlem2  23255  tchcph  23256  cphipval2  23260  4cphipval2  23261  cphipval  23262  pjthlem1  23430  mdegvscale  24059  mdegvsca  24060  plypf1  24192  ttgcontlem1  25989  sitgclbn  30740  lindsenlbs  33723  lfl0  34851  lflsub  34853  lflmul  34854  lfl0f  34855  lfl1  34856  lfladdcl  34857  lflnegcl  34861  lflvscl  34863  lkrlss  34881  eqlkr  34885  lkrlsp  34888  lshpkrlem4  34899  lshpkrlem5  34900  lshpkrlem6  34901  lclkrlem2m  37305  lclkrlem2p  37308  lcdvscl  37391  baerlem3lem1  37493  baerlem5alem1  37494  baerlem5blem1  37495  hdmap14lem1a  37652  hdmap14lem2a  37653  hdmap14lem2N  37655  hdmap14lem3  37656  hdmap14lem4a  37657  hdmap14lem8  37661  hgmapadd  37680  hgmapmul  37681  hgmaprnlem4N  37685  hgmap11  37688  hdmapgln2  37698  hdmapinvlem3  37706  hdmapinvlem4  37707  hdmapglem7b  37714  hlhilphllem  37745  mendassa  38270  ply1mulgsum  42751  lincfsuppcl  42775  linccl  42776  lincvalsng  42778  lincvalpr  42780  lincdifsn  42786  linc1  42787  lincsum  42791  lincscm  42792  lincscmcl  42794  lincext3  42818  lindslinindimp2lem4  42823  lindslinindsimp2  42825  snlindsntor  42833  lincresunit3lem2  42842  lincresunit3  42843  zlmodzxzldeplem3  42864
  Copyright terms: Public domain W3C validator