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

Theorem lmodvacl 17088
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 17081 . 2  |-  ( W  e.  LMod  ->  W  e. 
Grp )
2 lmodvacl.v . . 3  |-  V  =  ( Base `  W
)
3 lmodvacl.a . . 3  |-  .+  =  ( +g  `  W )
42, 3grpcl 15673 . 2  |-  ( ( W  e.  Grp  /\  X  e.  V  /\  Y  e.  V )  ->  ( X  .+  Y
)  e.  V )
51, 4syl3an1 1252 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 965    = wceq 1370    e. wcel 1758   ` cfv 5529  (class class class)co 6203   Basecbs 14295   +g cplusg 14360   Grpcgrp 15532   LModclmod 17074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4532  ax-pow 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-mnd 15537  df-grp 15667  df-lmod 17076
This theorem is referenced by:  lmodcom  17117  lmodvsghm  17132  lss1  17146  lspprabs  17302  lspabs2  17327  lspabs3  17328  lspfixed  17335  lspexch  17336  lspsolvlem  17349  ipdir  18196  ipdi  18197  ip2di  18198  ocvlss  18225  frlmphl  18334  frlmup1  18354  nmparlem  20889  minveclem2  21048  lincsumcl  31117  lsatfixedN  33012  lfl0f  33072  lfladdcl  33074  lflnegcl  33078  lflvscl  33080  lkrlss  33098  lshpkrlem5  33117  lshpkrlem6  33118  dvh3dim2  35451  dvh3dim3N  35452  lcfrlem17  35562  lcfrlem19  35564  lcfrlem20  35565  lcfrlem23  35568  baerlem3lem1  35710  baerlem5alem1  35711  baerlem5blem1  35712  baerlem5alem2  35714  baerlem5blem2  35715  mapdindp0  35722  mapdindp2  35724  mapdindp4  35726  mapdh6lem2N  35737  mapdh6aN  35738  mapdh6dN  35742  mapdh6eN  35743  mapdh6hN  35746  hdmap1l6lem2  35812  hdmap1l6a  35813  hdmap1l6d  35817  hdmap1l6e  35818  hdmap1l6h  35821  hdmap11lem1  35847  hdmap11lem2  35848  hdmapneg  35852  hdmaprnlem3N  35856  hdmaprnlem3uN  35857  hdmaprnlem6N  35860  hdmaprnlem7N  35861  hdmaprnlem9N  35863  hdmaprnlem3eN  35864  hdmap14lem10  35883  hdmapinvlem3  35926  hdmapinvlem4  35927  hdmapglem7b  35934  hlhilphllem  35965
  Copyright terms: Public domain W3C validator