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

Theorem lmodvacl 17338
Description: Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypotheses
Ref Expression
lmodvacl.v  |-  V  =  ( Base `  W
)
lmodvacl.a  |-  .+  =  ( +g  `  W )
Assertion
Ref Expression
lmodvacl  |-  ( ( W  e.  LMod  /\  X  e.  V  /\  Y  e.  V )  ->  ( X  .+  Y )  e.  V )

Proof of Theorem lmodvacl
StepHypRef Expression
1 lmodgrp 17331 . 2  |-  ( W  e.  LMod  ->  W  e. 
Grp )
2 lmodvacl.v . . 3  |-  V  =  ( Base `  W
)
3 lmodvacl.a . . 3  |-  .+  =  ( +g  `  W )
42, 3grpcl 15877 . 2  |-  ( ( W  e.  Grp  /\  X  e.  V  /\  Y  e.  V )  ->  ( X  .+  Y
)  e.  V )
51, 4syl3an1 1261 1  |-  ( ( W  e.  LMod  /\  X  e.  V  /\  Y  e.  V )  ->  ( X  .+  Y )  e.  V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973    = wceq 1379    e. wcel 1767   ` cfv 5588  (class class class)co 6285   Basecbs 14493   +g cplusg 14558   Grpcgrp 15730   LModclmod 17324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576  ax-pow 4625
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6288  df-mnd 15735  df-grp 15871  df-lmod 17326
This theorem is referenced by:  lmodcom  17368  lmodvsghm  17383  lss1  17397  lspprabs  17553  lspabs2  17578  lspabs3  17579  lspfixed  17586  lspexch  17587  lspsolvlem  17600  ipdir  18481  ipdi  18482  ip2di  18483  ocvlss  18510  frlmphl  18619  frlmup1  18639  nmparlem  21509  minveclem2  21668  lincsumcl  32330  lsatfixedN  34023  lfl0f  34083  lfladdcl  34085  lflnegcl  34089  lflvscl  34091  lkrlss  34109  lshpkrlem5  34128  lshpkrlem6  34129  dvh3dim2  36462  dvh3dim3N  36463  lcfrlem17  36573  lcfrlem19  36575  lcfrlem20  36576  lcfrlem23  36579  baerlem3lem1  36721  baerlem5alem1  36722  baerlem5blem1  36723  baerlem5alem2  36725  baerlem5blem2  36726  mapdindp0  36733  mapdindp2  36735  mapdindp4  36737  mapdh6lem2N  36748  mapdh6aN  36749  mapdh6dN  36753  mapdh6eN  36754  mapdh6hN  36757  hdmap1l6lem2  36823  hdmap1l6a  36824  hdmap1l6d  36828  hdmap1l6e  36829  hdmap1l6h  36832  hdmap11lem1  36858  hdmap11lem2  36859  hdmapneg  36863  hdmaprnlem3N  36867  hdmaprnlem3uN  36868  hdmaprnlem6N  36871  hdmaprnlem7N  36872  hdmaprnlem9N  36874  hdmaprnlem3eN  36875  hdmap14lem10  36894  hdmapinvlem3  36937  hdmapinvlem4  36938  hdmapglem7b  36945  hlhilphllem  36976
  Copyright terms: Public domain W3C validator