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

Theorem lmodvscl 15967
Description: Closure of scalar product for a left module. (hvmulcl 22516 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 2436 . . . . 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 2436 . . . . 5  |-  ( +g  `  F )  =  ( +g  `  F )
10 eqid 2436 . . . . 5  |-  ( .r
`  F )  =  ( .r `  F
)
11 eqid 2436 . . . . 5  |-  ( 1r
`  F )  =  ( 1r `  F
)
124, 5, 6, 7, 8, 9, 10, 11lmodlema 15955 . . . 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 1652    e. wcel 1725   ` cfv 5454  (class class class)co 6081   Basecbs 13469   +g cplusg 13529   .rcmulr 13530  Scalarcsca 13532   .scvsca 13533   1rcur 15662   LModclmod 15950
This theorem is referenced by:  lmodscaf  15972  lmod0vs  15983  lmodvneg1  15987  lmodvsneg  15988  lmodnegadd  15993  lmodsubvs  16000  lmodsubdi  16001  lmodsubdir  16002  lmodvsghm  16005  lmodprop2d  16006  lss1  16015  lssvsubcl  16020  lssvscl  16031  lss1d  16039  lssacs  16043  prdsvscacl  16044  lmodvsinv  16112  lmodvsinv2  16113  islmhm2  16114  0lmhm  16116  idlmhm  16117  lmhmco  16119  lmhmplusg  16120  lmhmvsca  16121  lmhmf1o  16122  lmhmpreima  16124  lmhmeql  16131  pwsdiaglmhm  16133  lvecvscan  16183  lvecvscan2  16184  lspsnvs  16186  lspfixed  16200  lspexch  16201  lspsolvlem  16214  lspsolv  16215  islbs2  16226  assapropd  16386  asclf  16396  asclrhm  16400  mplcoe1  16528  mplmon2cl  16560  mplmon2mul  16561  mplind  16562  ply1tmcl  16664  ply1coe  16684  ipass  16876  ipassr  16877  ocvlss  16899  nlmdsdi  18717  nlmdsdir  18718  nlmmul0or  18719  nlmvscnlem2  18721  nlmvscn  18723  nmoleub2lem3  19123  nmoleub3  19127  cph2ass  19175  ipcau2  19191  tchcphlem2  19193  tchcph  19194  pjthlem1  19338  mdegvscale  19998  mdegvsca  19999  plypf1  20131  sitgclbn  24657  lcomf  26746  pwssplit3  27167  dsmmlss  27187  uvcresum  27219  frlmssuvc2  27224  frlmup1  27227  lindfmm  27274  islindf4  27285  mendassa  27479  lfl0  29863  lflsub  29865  lflmul  29866  lfl0f  29867  lfl1  29868  lfladdcl  29869  lflnegcl  29873  lflvscl  29875  lkrlss  29893  eqlkr  29897  lkrlsp  29900  lshpkrlem4  29911  lshpkrlem5  29912  lshpkrlem6  29913  lclkrlem2m  32317  lclkrlem2p  32320  lcdvscl  32403  baerlem3lem1  32505  baerlem5alem1  32506  baerlem5blem1  32507  hdmap14lem1a  32667  hdmap14lem2a  32668  hdmap14lem2N  32670  hdmap14lem3  32671  hdmap14lem4a  32672  hdmap14lem8  32676  hgmapadd  32695  hgmapmul  32696  hgmaprnlem4N  32700  hgmap11  32703  hdmapgln2  32713  hdmapinvlem3  32721  hdmapinvlem4  32722  hdmapglem7b  32729  hlhilphllem  32760
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-lmod 15952
  Copyright terms: Public domain W3C validator