Theorem lmodvacl 18877

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

Step	Hyp	Ref	Expression
1		lmodgrp 18870	. 2 |- ( W e. LMod -> W e. Grp )
2		lmodvacl.v	. . 3 |- V = ( Base ` W )
3		lmodvacl.a	. . 3 |- .+ = ( +g ` W )
4	2, 3	grpcl 17430	. 2 |- ( ( W e. Grp /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
5	1, 4	syl3an1 1359	1 |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )

Syntax hints:   -> wi 4   /\ w3a 1037   = wceq 1483   e. wcel 1990   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   Grpcgrp 17422   LModclmod 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-lmod 18865

This theorem is referenced by:  lmodcom  18909  lmodvsghm  18924  lss1  18939  lspprabs  19095  lspabs2  19120  lspabs3  19121  lspfixed  19128  lspexch  19129  lspsolvlem  19142  ipdir  19984  ipdi  19985  ip2di  19986  ocvlss  20016  frlmphl  20120  frlmup1  20137  nmparlem  23038  minveclem2  23197  lsatfixedN  34296  lfl0f  34356  lfladdcl  34358  lflnegcl  34362  lflvscl  34364  lkrlss  34382  lshpkrlem5  34401  lshpkrlem6  34402  dvh3dim2  36737  dvh3dim3N  36738  lcfrlem17  36848  lcfrlem19  36850  lcfrlem20  36851  lcfrlem23  36854  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  baerlem5alem2  37000  baerlem5blem2  37001  mapdindp0  37008  mapdindp2  37010  mapdindp4  37012  mapdh6lem2N  37023  mapdh6aN  37024  mapdh6dN  37028  mapdh6eN  37029  mapdh6hN  37032  hdmap1l6lem2  37098  hdmap1l6a  37099  hdmap1l6d  37103  hdmap1l6e  37104  hdmap1l6h  37107  hdmap11lem1  37133  hdmap11lem2  37134  hdmapneg  37138  hdmaprnlem3N  37142  hdmaprnlem3uN  37143  hdmaprnlem6N  37146  hdmaprnlem7N  37147  hdmaprnlem9N  37149  hdmaprnlem3eN  37150  hdmap14lem10  37169  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem7b  37220  hlhilphllem  37251  lincsumcl  42220