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

Theorem lmodvscl 19571
 Description: Closure of scalar product for a left module. (hvmulcl 28704 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 2826 . . . . 5 (+g𝑊) = (+g𝑊)
6 lmodvscl.s . . . . 5 · = ( ·𝑠𝑊)
7 lmodvscl.f . . . . 5 𝐹 = (Scalar‘𝑊)
8 lmodvscl.k . . . . 5 𝐾 = (Base‘𝐹)
9 eqid 2826 . . . . 5 (+g𝐹) = (+g𝐹)
10 eqid 2826 . . . . 5 (.r𝐹) = (.r𝐹)
11 eqid 2826 . . . . 5 (1r𝐹) = (1r𝐹)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 19559 . . . 4 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
1312simpld 495 . . 3 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋))))
1413simp1d 1136 . 2 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
151, 2, 3, 14syl3anb 1155 1 ((𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ‘cfv 6352  (class class class)co 7148  Basecbs 16473  +gcplusg 16555  .rcmulr 16556  Scalarcsca 16558   ·𝑠 cvsca 16559  1rcur 19171  LModclmod 19554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-nul 5207 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360  df-ov 7151  df-lmod 19556 This theorem is referenced by:  lmodscaf  19576  lmod0vs  19587  lmodvsmmulgdi  19589  lcomf  19593  lmodvneg1  19597  lmodvsneg  19598  lmodnegadd  19603  lmodsubvs  19610  lmodsubdi  19611  lmodsubdir  19612  lmodvsghm  19615  lmodprop2d  19616  lss1  19630  lssvsubcl  19635  lssvscl  19647  lss1d  19655  lssacs  19659  prdsvscacl  19660  lmodvsinv  19728  lmodvsinv2  19729  islmhm2  19730  0lmhm  19732  idlmhm  19733  lmhmco  19735  lmhmplusg  19736  lmhmvsca  19737  lmhmf1o  19738  lmhmpreima  19740  lmhmeql  19747  pwsdiaglmhm  19749  pwssplit3  19753  lvecvscan  19803  lvecvscan2  19804  lspsnvs  19806  lspfixed  19820  lspexch  19821  lspsolvlem  19834  lspsolv  19835  islbs2  19846  assa2ass  20014  assapropd  20020  asclf  20030  ascldimulOLD  20036  assamulgscmlem1  20047  assamulgscmlem2  20048  mplcoe1  20164  mplmon2cl  20198  mplmon2mul  20199  mplind  20200  mhpvscacl  20258  ply1tmcl  20357  ply1coe  20381  evl1gsummon  20444  ipass  20705  ipassr  20706  phlssphl  20719  ocvlss  20732  dsmmlss  20804  frlmvscavalb  20830  frlmvplusgscavalb  20831  frlmphl  20841  uvcresum  20853  frlmssuvc2  20855  frlmup1  20858  lindfmm  20887  islindf4  20898  matvscl  20956  mat0dimscm  20994  matinv  21202  mply1topmatcl  21329  pm2mpmhmlem2  21343  monmat2matmon  21348  chpmat1dlem  21359  chpmat1d  21360  chpdmatlem0  21361  chfacfscmulcl  21381  cpmadugsumlemB  21398  cpmadugsumlemC  21399  cpmadugsumlemF  21400  cpmadugsumfi  21401  cpmidgsum2  21403  nlmdsdi  23205  nlmdsdir  23206  nlmmul0or  23207  nlmvscnlem2  23209  nlmvscn  23211  clmvscl  23607  cmodscmulexp  23641  cph2ass  23732  ipcau2  23752  tcphcphlem2  23754  tcphcph  23755  cphipval2  23759  4cphipval2  23760  cphipval  23761  pjthlem1  23955  mdegvscale  24584  mdegvsca  24585  plypf1  24717  ttgcontlem1  26585  lmodvslmhm  30602  eqgvscpbl  30833  qusvscpbl  30834  qusscaval  30835  imaslmod  30836  linds2eq  30855  tngdim  30897  matdim  30899  lindsunlem  30906  lbsdiflsp0  30908  fedgmullem1  30911  fedgmullem2  30912  sitgclbn  31487  lindsadd  34752  lindsenlbs  34754  lfl0  36068  lflsub  36070  lflmul  36071  lfl0f  36072  lfl1  36073  lfladdcl  36074  lflnegcl  36078  lflvscl  36080  lkrlss  36098  eqlkr  36102  lkrlsp  36105  lshpkrlem4  36116  lshpkrlem5  36117  lshpkrlem6  36118  lclkrlem2m  38522  lclkrlem2p  38525  lcdvscl  38608  baerlem3lem1  38710  baerlem5alem1  38711  baerlem5blem1  38712  hdmap14lem1a  38869  hdmap14lem2a  38870  hdmap14lem2N  38872  hdmap14lem3  38873  hdmap14lem4a  38874  hdmap14lem8  38878  hgmapadd  38897  hgmapmul  38898  hgmaprnlem4N  38902  hgmap11  38905  hdmapgln2  38915  hdmapinvlem3  38923  hdmapinvlem4  38924  hdmapglem7b  38931  hlhilphllem  38962  frlmsnic  39014  prjspvs  39125  prjspeclsp  39127  mendassa  39659  ply1mulgsum  44276  lincfsuppcl  44300  linccl  44301  lincvalsng  44303  lincvalpr  44305  lincdifsn  44311  linc1  44312  lincsum  44316  lincscm  44317  lincscmcl  44319  lincext3  44343  lindslinindimp2lem4  44348  lindslinindsimp2  44350  snlindsntor  44358  lincresunit3lem2  44367  lincresunit3  44368  zlmodzxzldeplem3  44389
 Copyright terms: Public domain W3C validator