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

Theorem lmodvscl 15644
Description: Closure of scalar product for a left module. (hvmulcl 21593 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lmodvscl.v  |-  V  =  ( Base `  W
)
lmodvscl.f  |-  F  =  (Scalar `  W )
lmodvscl.s  |-  .x.  =  ( .s `  W )
lmodvscl.k  |-  K  =  ( Base `  F
)
Assertion
Ref Expression
lmodvscl  |-  ( ( W  e.  LMod  /\  R  e.  K  /\  X  e.  V )  ->  ( R  .x.  X )  e.  V )

Proof of Theorem lmodvscl
StepHypRef Expression
1 biid 227 . 2  |-  ( W  e.  LMod  <->  W  e.  LMod )
2 pm4.24 624 . 2  |-  ( R  e.  K  <->  ( R  e.  K  /\  R  e.  K ) )
3 pm4.24 624 . 2  |-  ( X  e.  V  <->  ( X  e.  V  /\  X  e.  V ) )
4 lmodvscl.v . . . . 5  |-  V  =  ( Base `  W
)
5 eqid 2283 . . . . 5  |-  ( +g  `  W )  =  ( +g  `  W )
6 lmodvscl.s . . . . 5  |-  .x.  =  ( .s `  W )
7 lmodvscl.f . . . . 5  |-  F  =  (Scalar `  W )
8 lmodvscl.k . . . . 5  |-  K  =  ( Base `  F
)
9 eqid 2283 . . . . 5  |-  ( +g  `  F )  =  ( +g  `  F )
10 eqid 2283 . . . . 5  |-  ( .r
`  F )  =  ( .r `  F
)
11 eqid 2283 . . . . 5  |-  ( 1r
`  F )  =  ( 1r `  F
)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 15632 . . . 4  |-  ( ( W  e.  LMod  /\  ( R  e.  K  /\  R  e.  K )  /\  ( X  e.  V  /\  X  e.  V
) )  ->  (
( ( R  .x.  X )  e.  V  /\  ( R  .x.  ( X ( +g  `  W
) X ) )  =  ( ( R 
.x.  X ) ( +g  `  W ) ( R  .x.  X
) )  /\  (
( R ( +g  `  F ) R ) 
.x.  X )  =  ( ( R  .x.  X ) ( +g  `  W ) ( R 
.x.  X ) ) )  /\  ( ( ( R ( .r
`  F ) R )  .x.  X )  =  ( R  .x.  ( R  .x.  X ) )  /\  ( ( 1r `  F ) 
.x.  X )  =  X ) ) )
1312simpld 445 . . 3  |-  ( ( W  e.  LMod  /\  ( R  e.  K  /\  R  e.  K )  /\  ( X  e.  V  /\  X  e.  V
) )  ->  (
( R  .x.  X
)  e.  V  /\  ( R  .x.  ( X ( +g  `  W
) X ) )  =  ( ( R 
.x.  X ) ( +g  `  W ) ( R  .x.  X
) )  /\  (
( R ( +g  `  F ) R ) 
.x.  X )  =  ( ( R  .x.  X ) ( +g  `  W ) ( R 
.x.  X ) ) ) )
1413simp1d 967 . 2  |-  ( ( W  e.  LMod  /\  ( R  e.  K  /\  R  e.  K )  /\  ( X  e.  V  /\  X  e.  V
) )  ->  ( R  .x.  X )  e.  V )
151, 2, 3, 14syl3anb 1225 1  |-  ( ( W  e.  LMod  /\  R  e.  K  /\  X  e.  V )  ->  ( R  .x.  X )  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   .scvsca 13212   1rcur 15339   LModclmod 15627
This theorem is referenced by:  lmodscaf  15649  lmod0vs  15663  lmodvneg1  15667  lmodvsnegOLD  15668  lmodvsneg  15669  lmodnegadd  15674  lmodsubvs  15681  lmodsubdi  15682  lmodsubdir  15683  lmodvsghm  15686  lmodprop2d  15687  lss1  15696  lssvsubcl  15701  lssvscl  15712  lss1d  15720  lssacs  15724  prdsvscacl  15725  lmodvsinv  15793  lmodvsinv2  15794  islmhm2  15795  0lmhm  15797  idlmhm  15798  lmhmco  15800  lmhmplusg  15801  lmhmvsca  15802  lmhmf1o  15803  lmhmpreima  15805  lmhmeql  15812  pwsdiaglmhm  15814  lvecvscan  15864  lvecvscan2  15865  lspsnvs  15867  lspfixed  15881  lspexch  15882  lspsolvlem  15895  lspsolv  15896  islbs2  15907  assapropd  16067  asclf  16077  asclrhm  16081  mplcoe1  16209  mplmon2cl  16241  mplmon2mul  16242  mplind  16243  ply1tmcl  16348  ply1coe  16368  ipass  16549  ipassr  16550  ocvlss  16572  nlmdsdi  18192  nlmdsdir  18193  nlmmul0or  18194  nlmvscnlem2  18196  nlmvscn  18198  nmoleub2lem3  18596  nmoleub3  18600  cph2ass  18648  ipcau2  18664  tchcphlem2  18666  tchcph  18667  pjthlem1  18801  mdegvscale  19461  mdegvsca  19462  plypf1  19594  lcomf  26767  pwssplit3  27190  dsmmlss  27210  uvcresum  27242  frlmssuvc2  27247  frlmup1  27250  lindfmm  27297  islindf4  27308  mendassa  27502  lfl0  29255  lflsub  29257  lflmul  29258  lfl0f  29259  lfl1  29260  lfladdcl  29261  lflnegcl  29265  lflvscl  29267  lkrlss  29285  eqlkr  29289  lkrlsp  29292  lshpkrlem4  29303  lshpkrlem5  29304  lshpkrlem6  29305  lclkrlem2m  31709  lclkrlem2p  31712  lcdvscl  31795  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  hdmap14lem1a  32059  hdmap14lem2a  32060  hdmap14lem2N  32062  hdmap14lem3  32063  hdmap14lem4a  32064  hdmap14lem8  32068  hgmapadd  32087  hgmapmul  32088  hgmaprnlem4N  32092  hgmap11  32095  hdmapgln2  32105  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem7b  32121  hlhilphllem  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lmod 15629
  Copyright terms: Public domain W3C validator