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

Theorem lmodvscl 15660
Description: Closure of scalar product for a left module. (hvmulcl 21609 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 2296 . . . . 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 2296 . . . . 5  |-  ( +g  `  F )  =  ( +g  `  F )
10 eqid 2296 . . . . 5  |-  ( .r
`  F )  =  ( .r `  F
)
11 eqid 2296 . . . . 5  |-  ( 1r
`  F )  =  ( 1r `  F
)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 15648 . . . 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 1632    e. wcel 1696   ` cfv 5271  (class class class)co 5874   Basecbs 13164   +g cplusg 13224   .rcmulr 13225  Scalarcsca 13227   .scvsca 13228   1rcur 15355   LModclmod 15643
This theorem is referenced by:  lmodscaf  15665  lmod0vs  15679  lmodvneg1  15683  lmodvsnegOLD  15684  lmodvsneg  15685  lmodnegadd  15690  lmodsubvs  15697  lmodsubdi  15698  lmodsubdir  15699  lmodvsghm  15702  lmodprop2d  15703  lss1  15712  lssvsubcl  15717  lssvscl  15728  lss1d  15736  lssacs  15740  prdsvscacl  15741  lmodvsinv  15809  lmodvsinv2  15810  islmhm2  15811  0lmhm  15813  idlmhm  15814  lmhmco  15816  lmhmplusg  15817  lmhmvsca  15818  lmhmf1o  15819  lmhmpreima  15821  lmhmeql  15828  pwsdiaglmhm  15830  lvecvscan  15880  lvecvscan2  15881  lspsnvs  15883  lspfixed  15897  lspexch  15898  lspsolvlem  15911  lspsolv  15912  islbs2  15923  assapropd  16083  asclf  16093  asclrhm  16097  mplcoe1  16225  mplmon2cl  16257  mplmon2mul  16258  mplind  16259  ply1tmcl  16364  ply1coe  16384  ipass  16565  ipassr  16566  ocvlss  16588  nlmdsdi  18208  nlmdsdir  18209  nlmmul0or  18210  nlmvscnlem2  18212  nlmvscn  18214  nmoleub2lem3  18612  nmoleub3  18616  cph2ass  18664  ipcau2  18680  tchcphlem2  18682  tchcph  18683  pjthlem1  18817  mdegvscale  19477  mdegvsca  19478  plypf1  19610  lcomf  26870  pwssplit3  27293  dsmmlss  27313  uvcresum  27345  frlmssuvc2  27350  frlmup1  27353  lindfmm  27400  islindf4  27411  mendassa  27605  lfl0  29877  lflsub  29879  lflmul  29880  lfl0f  29881  lfl1  29882  lfladdcl  29883  lflnegcl  29887  lflvscl  29889  lkrlss  29907  eqlkr  29911  lkrlsp  29914  lshpkrlem4  29925  lshpkrlem5  29926  lshpkrlem6  29927  lclkrlem2m  32331  lclkrlem2p  32334  lcdvscl  32417  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  hdmap14lem1a  32681  hdmap14lem2a  32682  hdmap14lem2N  32684  hdmap14lem3  32685  hdmap14lem4a  32686  hdmap14lem8  32690  hgmapadd  32709  hgmapmul  32710  hgmaprnlem4N  32714  hgmap11  32717  hdmapgln2  32727  hdmapinvlem3  32735  hdmapinvlem4  32736  hdmapglem7b  32743  hlhilphllem  32774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-lmod 15645
  Copyright terms: Public domain W3C validator