MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvscl Structured version   Visualization version   GIF version
Theorem lmodvscl 20481
Description: Closure of scalar product for a left module. (hvmulcl 30253 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 260 . 2 (π‘Š ∈ LMod ↔ π‘Š ∈ LMod)
2 pm4.24 564 . 2 (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3 pm4.24 564 . 2 (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4 lmodvscl.v . . . . 5 𝑉 = (Baseβ€˜π‘Š)
5 eqid 2732 . . . . 5 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
6 lmodvscl.s . . . . 5 Β· = ( ·𝑠 β€˜π‘Š)
7 lmodvscl.f . . . . 5 𝐹 = (Scalarβ€˜π‘Š)
8 lmodvscl.k . . . . 5 𝐾 = (Baseβ€˜πΉ)
9 eqid 2732 . . . . 5 (+gβ€˜πΉ) = (+gβ€˜πΉ)
10 eqid 2732 . . . . 5 (.rβ€˜πΉ) = (.rβ€˜πΉ)
11 eqid 2732 . . . . 5 (1rβ€˜πΉ) = (1rβ€˜πΉ)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 20468 . . . 4 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋(+gβ€˜π‘Š)𝑋)) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋)) ∧ ((𝑅(+gβ€˜πΉ)𝑅) Β· 𝑋) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋))) ∧ (((𝑅(.rβ€˜πΉ)𝑅) Β· 𝑋) = (𝑅 Β· (𝑅 Β· 𝑋)) ∧ ((1rβ€˜πΉ) Β· 𝑋) = 𝑋)))
1312simpld 495 . . 3 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋(+gβ€˜π‘Š)𝑋)) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋)) ∧ ((𝑅(+gβ€˜πΉ)𝑅) Β· 𝑋) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋))))
1413simp1d 1142 . 2 ((π‘Š ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (𝑅 Β· 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1161 1 ((π‘Š ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) β†’ (𝑅 Β· 𝑋) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  +gcplusg 17193  .rcmulr 17194  Scalarcsca 17196   ·𝑠 cvsca 17197  1rcur 19998  LModclmod 20463
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-lmod 20465
This theorem is referenced by:  lmodscaf  20486  lmod0vs  20497  lmodvsmmulgdi  20499  lcomf  20503  lmodvneg1  20507  lmodvsneg  20508  lmodnegadd  20513  lmodsubvs  20520  lmodsubdi  20521  lmodsubdir  20522  lmodvsghm  20525  lmodprop2d  20526  lss1  20541  lssvsubcl  20546  lssvscl  20558  lss1d  20566  lssacs  20570  prdsvscacl  20571  lmodvsinv  20639  lmodvsinv2  20640  islmhm2  20641  0lmhm  20643  idlmhm  20644  lmhmco  20646  lmhmplusg  20647  lmhmvsca  20648  lmhmf1o  20649  lmhmpreima  20651  lmhmeql  20658  pwsdiaglmhm  20660  pwssplit3  20664  lvecvscan  20716  lvecvscan2  20717  lspsnvs  20719  lspfixed  20733  lspexch  20734  lspsolvlem  20747  lspsolv  20748  islbs2  20759  ipass  21189  ipassr  21190  phlssphl  21203  ocvlss  21216  dsmmlss  21290  frlmvscavalb  21316  frlmvplusgscavalb  21317  frlmphl  21327  uvcresum  21339  frlmssuvc2  21341  frlmup1  21344  lindfmm  21373  islindf4  21384  assa2ass  21409  assapropd  21417  asclf  21427  assamulgscmlem1  21444  assamulgscmlem2  21445  mplcoe1  21583  mplmon2cl  21620  mplmon2mul  21621  mplind  21622  mhpvscacl  21688  ply1tmcl  21785  ply1coe  21811  evl1gsummon  21875  matvscl  21924  mat0dimscm  21962  matinv  22170  mply1topmatcl  22298  pm2mpmhmlem2  22312  monmat2matmon  22317  chpmat1dlem  22328  chpmat1d  22329  chpdmatlem0  22330  chfacfscmulcl  22350  cpmadugsumlemB  22367  cpmadugsumlemC  22368  cpmadugsumlemF  22369  cpmadugsumfi  22370  cpmidgsum2  22372  nlmdsdi  24189  nlmdsdir  24190  nlmmul0or  24191  nlmvscnlem2  24193  nlmvscn  24195  clmvscl  24595  cmodscmulexp  24629  cph2ass  24721  ipcau2  24742  tcphcphlem2  24744  tcphcph  24745  cphipval2  24749  4cphipval2  24750  cphipval  24751  pjthlem1  24945  mdegvscale  25584  mdegvsca  25585  plypf1  25717  ttgcontlem1  28131  lmodvslmhm  32189  eqgvscpbl  32453  qusvscpbl  32454  qusvsval  32455  imaslmod  32456  linds2eq  32485  lmhmqusker  32522  evls1fpws  32634  evls1vsca  32638  asclply1subcl  32648  ply1degltlss  32655  gsummoncoe1fzo  32656  tngdim  32686  matdim  32688  ply1degltdimlem  32695  lindsunlem  32697  lbsdiflsp0  32699  fedgmullem1  32702  fedgmullem2  32703  evls1maplmhm  32748  sitgclbn  33330  lindsadd  36469  lindsenlbs  36471  lfl0  37923  lflsub  37925  lflmul  37926  lfl0f  37927  lfl1  37928  lfladdcl  37929  lflnegcl  37933  lflvscl  37935  lkrlss  37953  eqlkr  37957  lkrlsp  37960  lshpkrlem4  37971  lshpkrlem5  37972  lshpkrlem6  37973  lclkrlem2m  40378  lclkrlem2p  40381  lcdvscl  40464  baerlem3lem1  40566  baerlem5alem1  40567  baerlem5blem1  40568  hdmap14lem1a  40725  hdmap14lem2a  40726  hdmap14lem2N  40728  hdmap14lem3  40729  hdmap14lem4a  40730  hdmap14lem8  40734  hgmapadd  40753  hgmapmul  40754  hgmaprnlem4N  40758  hgmap11  40761  hdmapgln2  40771  hdmapinvlem3  40779  hdmapinvlem4  40780  hdmapglem7b  40787  hlhilphllem  40822  lmodvscld  41101  mendassa  41921  ply1mulgsum  47024  lincfsuppcl  47047  linccl  47048  lincvalsng  47050  lincvalpr  47052  lincdifsn  47058  linc1  47059  lincsum  47063  lincscm  47064  lincscmcl  47066  lincext3  47090  lindslinindimp2lem4  47095  lindslinindsimp2  47097  snlindsntor  47105  lincresunit3lem2  47114  lincresunit3  47115  zlmodzxzldeplem3  47136
  Copyright terms: Public domain W3C validator