Theorem lmodvacl 20870

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	⊢ 𝑉 = (Base‘𝑊)
lmodvacl.a	⊢ + = (+g‘𝑊)

Assertion

Ref	Expression
lmodvacl	⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)

Proof of Theorem lmodvacl

Step	Hyp	Ref	Expression
1		lmodgrp 20862	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		lmodvacl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lmodvacl.a	. . 3 ⊢ + = (+g‘𝑊)
4	2, 3	grpcl 18917	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
5	1, 4	syl3an1 1164	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  Grpcgrp 18909  LModclmod 20855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-grp 18912  df-lmod 20857

This theorem is referenced by:  lmodcom  20903  lmodvsghm  20918  lss1  20933  lspprabs  21090  lspabs2  21118  lspabs3  21119  lspfixed  21126  lspexch  21127  lspsolvlem  21140  ipdir  21619  ipdi  21620  ip2di  21621  ocvlss  21652  frlmphl  21761  frlmup1  21778  nmparlem  25206  minveclem2  25393  lsatfixedN  39455  lfl0f  39515  lfladdcl  39517  lflnegcl  39521  lflvscl  39523  lkrlss  39541  lshpkrlem5  39560  lshpkrlem6  39561  dvh3dim2  41894  dvh3dim3N  41895  lcfrlem17  42005  lcfrlem19  42007  lcfrlem20  42008  lcfrlem23  42011  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem5alem2  42157  baerlem5blem2  42158  mapdindp0  42165  mapdindp2  42167  mapdindp4  42169  mapdh6lem2N  42180  mapdh6aN  42181  mapdh6dN  42185  mapdh6eN  42186  mapdh6hN  42189  hdmap1l6lem2  42254  hdmap1l6a  42255  hdmap1l6d  42259  hdmap1l6e  42260  hdmap1l6h  42263  hdmap11lem1  42287  hdmap11lem2  42288  hdmapneg  42292  hdmaprnlem3N  42296  hdmaprnlem3uN  42297  hdmaprnlem6N  42300  hdmaprnlem7N  42301  hdmaprnlem9N  42303  hdmaprnlem3eN  42304  hdmap14lem10  42323  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem7b  42374  hlhilphllem  42405  frlmsnic  42985  lincsumcl  48907