MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvscl Structured version   Visualization version   GIF version
Theorem lmodvscl 20489
Description: Closure of scalar product for a left module. (hvmulcl 30266 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 261 . 2 (π‘Š ∈ LMod ↔ π‘Š ∈ LMod)
2 pm4.24 565 . 2 (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3 pm4.24 565 . 2 (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4 lmodvscl.v . . . . 5 𝑉 = (Baseβ€˜π‘Š)
5 eqid 2733 . . . . 5 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
6 lmodvscl.s . . . . 5 Β· = ( ·𝑠 β€˜π‘Š)
7 lmodvscl.f . . . . 5 𝐹 = (Scalarβ€˜π‘Š)
8 lmodvscl.k . . . . 5 𝐾 = (Baseβ€˜πΉ)
9 eqid 2733 . . . . 5 (+gβ€˜πΉ) = (+gβ€˜πΉ)
10 eqid 2733 . . . . 5 (.rβ€˜πΉ) = (.rβ€˜πΉ)
11 eqid 2733 . . . . 5 (1rβ€˜πΉ) = (1rβ€˜πΉ)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 20476 . . . 4 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋(+gβ€˜π‘Š)𝑋)) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋)) ∧ ((𝑅(+gβ€˜πΉ)𝑅) Β· 𝑋) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋))) ∧ (((𝑅(.rβ€˜πΉ)𝑅) Β· 𝑋) = (𝑅 Β· (𝑅 Β· 𝑋)) ∧ ((1rβ€˜πΉ) Β· 𝑋) = 𝑋)))
1312simpld 496 . . 3 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋(+gβ€˜π‘Š)𝑋)) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋)) ∧ ((𝑅(+gβ€˜πΉ)𝑅) Β· 𝑋) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋))))
1413simp1d 1143 . 2 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (𝑅 Β· 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1162 1 ((π‘Š ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) β†’ (𝑅 Β· 𝑋) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  Scalarcsca 17200   ·𝑠 cvsca 17201  1rcur 20004  LModclmod 20471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-lmod 20473
This theorem is referenced by:  lmodscaf  20494  lmod0vs  20505  lmodvsmmulgdi  20507  lcomf  20511  lmodvneg1  20515  lmodvsneg  20516  lmodnegadd  20521  lmodsubvs  20528  lmodsubdi  20529  lmodsubdir  20530  lmodvsghm  20533  lmodprop2d  20534  lss1  20549  lssvsubcl  20554  lssvscl  20566  lss1d  20574  lssacs  20578  prdsvscacl  20579  lmodvsinv  20647  lmodvsinv2  20648  islmhm2  20649  0lmhm  20651  idlmhm  20652  lmhmco  20654  lmhmplusg  20655  lmhmvsca  20656  lmhmf1o  20657  lmhmpreima  20659  lmhmeql  20666  pwsdiaglmhm  20668  pwssplit3  20672  lvecvscan  20724  lvecvscan2  20725  lspsnvs  20727  lspfixed  20741  lspexch  20742  lspsolvlem  20755  lspsolv  20756  islbs2  20767  ipass  21198  ipassr  21199  phlssphl  21212  ocvlss  21225  dsmmlss  21299  frlmvscavalb  21325  frlmvplusgscavalb  21326  frlmphl  21336  uvcresum  21348  frlmssuvc2  21350  frlmup1  21353  lindfmm  21382  islindf4  21393  assa2ass  21418  assapropd  21426  asclf  21436  assamulgscmlem1  21453  assamulgscmlem2  21454  mplcoe1  21592  mplmon2cl  21629  mplmon2mul  21630  mplind  21631  mhpvscacl  21697  ply1tmcl  21794  ply1coe  21820  evl1gsummon  21884  matvscl  21933  mat0dimscm  21971  matinv  22179  mply1topmatcl  22307  pm2mpmhmlem2  22321  monmat2matmon  22326  chpmat1dlem  22337  chpmat1d  22338  chpdmatlem0  22339  chfacfscmulcl  22359  cpmadugsumlemB  22376  cpmadugsumlemC  22377  cpmadugsumlemF  22378  cpmadugsumfi  22379  cpmidgsum2  22381  nlmdsdi  24198  nlmdsdir  24199  nlmmul0or  24200  nlmvscnlem2  24202  nlmvscn  24204  clmvscl  24604  cmodscmulexp  24638  cph2ass  24730  ipcau2  24751  tcphcphlem2  24753  tcphcph  24754  cphipval2  24758  4cphipval2  24759  cphipval  24760  pjthlem1  24954  mdegvscale  25593  mdegvsca  25594  plypf1  25726  ttgcontlem1  28142  lmodvslmhm  32202  eqgvscpbl  32465  qusvscpbl  32466  qusvsval  32467  imaslmod  32468  linds2eq  32497  lmhmqusker  32534  evls1fpws  32646  evls1vsca  32650  asclply1subcl  32660  ply1degltlss  32667  gsummoncoe1fzo  32668  tngdim  32698  matdim  32700  ply1degltdimlem  32707  lindsunlem  32709  lbsdiflsp0  32711  fedgmullem1  32714  fedgmullem2  32715  evls1maplmhm  32760  sitgclbn  33342  lindsadd  36481  lindsenlbs  36483  lfl0  37935  lflsub  37937  lflmul  37938  lfl0f  37939  lfl1  37940  lfladdcl  37941  lflnegcl  37945  lflvscl  37947  lkrlss  37965  eqlkr  37969  lkrlsp  37972  lshpkrlem4  37983  lshpkrlem5  37984  lshpkrlem6  37985  lclkrlem2m  40390  lclkrlem2p  40393  lcdvscl  40476  baerlem3lem1  40578  baerlem5alem1  40579  baerlem5blem1  40580  hdmap14lem1a  40737  hdmap14lem2a  40738  hdmap14lem2N  40740  hdmap14lem3  40741  hdmap14lem4a  40742  hdmap14lem8  40746  hgmapadd  40765  hgmapmul  40766  hgmaprnlem4N  40770  hgmap11  40773  hdmapgln2  40783  hdmapinvlem3  40791  hdmapinvlem4  40792  hdmapglem7b  40799  hlhilphllem  40834  lmodvscld  41104  mendassa  41936  ply1mulgsum  47071  lincfsuppcl  47094  linccl  47095  lincvalsng  47097  lincvalpr  47099  lincdifsn  47105  linc1  47106  lincsum  47110  lincscm  47111  lincscmcl  47113  lincext3  47137  lindslinindimp2lem4  47142  lindslinindsimp2  47144  snlindsntor  47152  lincresunit3lem2  47161  lincresunit3  47162  zlmodzxzldeplem3  47183
  Copyright terms: Public domain W3C validator