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

Theorem lmodvscl 15922
Description: Closure of scalar product for a left module. (hvmulcl 22469 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 228 . 2  |-  ( W  e.  LMod  <->  W  e.  LMod )
2 pm4.24 625 . 2  |-  ( R  e.  K  <->  ( R  e.  K  /\  R  e.  K ) )
3 pm4.24 625 . 2  |-  ( X  e.  V  <->  ( X  e.  V  /\  X  e.  V ) )
4 lmodvscl.v . . . . 5  |-  V  =  ( Base `  W
)
5 eqid 2404 . . . . 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 2404 . . . . 5  |-  ( +g  `  F )  =  ( +g  `  F )
10 eqid 2404 . . . . 5  |-  ( .r
`  F )  =  ( .r `  F
)
11 eqid 2404 . . . . 5  |-  ( 1r
`  F )  =  ( 1r `  F
)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 15910 . . . 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 446 . . 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 969 . 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 1227 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 359    /\ w3a 936    = wceq 1649    e. wcel 1721   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   .rcmulr 13485  Scalarcsca 13487   .scvsca 13488   1rcur 15617   LModclmod 15905
This theorem is referenced by:  lmodscaf  15927  lmod0vs  15938  lmodvneg1  15942  lmodvsneg  15943  lmodnegadd  15948  lmodsubvs  15955  lmodsubdi  15956  lmodsubdir  15957  lmodvsghm  15960  lmodprop2d  15961  lss1  15970  lssvsubcl  15975  lssvscl  15986  lss1d  15994  lssacs  15998  prdsvscacl  15999  lmodvsinv  16067  lmodvsinv2  16068  islmhm2  16069  0lmhm  16071  idlmhm  16072  lmhmco  16074  lmhmplusg  16075  lmhmvsca  16076  lmhmf1o  16077  lmhmpreima  16079  lmhmeql  16086  pwsdiaglmhm  16088  lvecvscan  16138  lvecvscan2  16139  lspsnvs  16141  lspfixed  16155  lspexch  16156  lspsolvlem  16169  lspsolv  16170  islbs2  16181  assapropd  16341  asclf  16351  asclrhm  16355  mplcoe1  16483  mplmon2cl  16515  mplmon2mul  16516  mplind  16517  ply1tmcl  16619  ply1coe  16639  ipass  16831  ipassr  16832  ocvlss  16854  nlmdsdi  18670  nlmdsdir  18671  nlmmul0or  18672  nlmvscnlem2  18674  nlmvscn  18676  nmoleub2lem3  19076  nmoleub3  19080  cph2ass  19128  ipcau2  19144  tchcphlem2  19146  tchcph  19147  pjthlem1  19291  mdegvscale  19951  mdegvsca  19952  plypf1  20084  sitgclbn  24610  lcomf  26636  pwssplit3  27058  dsmmlss  27078  uvcresum  27110  frlmssuvc2  27115  frlmup1  27118  lindfmm  27165  islindf4  27176  mendassa  27370  lfl0  29548  lflsub  29550  lflmul  29551  lfl0f  29552  lfl1  29553  lfladdcl  29554  lflnegcl  29558  lflvscl  29560  lkrlss  29578  eqlkr  29582  lkrlsp  29585  lshpkrlem4  29596  lshpkrlem5  29597  lshpkrlem6  29598  lclkrlem2m  32002  lclkrlem2p  32005  lcdvscl  32088  baerlem3lem1  32190  baerlem5alem1  32191  baerlem5blem1  32192  hdmap14lem1a  32352  hdmap14lem2a  32353  hdmap14lem2N  32355  hdmap14lem3  32356  hdmap14lem4a  32357  hdmap14lem8  32361  hgmapadd  32380  hgmapmul  32381  hgmaprnlem4N  32385  hgmap11  32388  hdmapgln2  32398  hdmapinvlem3  32406  hdmapinvlem4  32407  hdmapglem7b  32414  hlhilphllem  32445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-lmod 15907
  Copyright terms: Public domain W3C validator