Theorem lmodvacl 19195

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 19188	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		lmodvacl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lmodvacl.a	. . 3 ⊢ + = (+g‘𝑊)
4	2, 3	grpcl 17746	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
5	1, 4	syl3an1 1203	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ w3a 1108   = wceq 1653   ∈ wcel 2157  ‘cfv 6101  (class class class)co 6878  Basecbs 16184  +_gcplusg 16267  Grpcgrp 17738  LModclmod 19181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-mgm 17557  df-sgrp 17599  df-mnd 17610  df-grp 17741  df-lmod 19183

This theorem is referenced by:  lmodcom  19227  lmodvsghm  19242  lss1  19257  lspprabs  19416  lspabs2  19441  lspabs3  19442  lspfixed  19449  lspfixedOLD  19450  lspexch  19451  lspsolvlem  19464  ipdir  20308  ipdi  20309  ip2di  20310  ocvlss  20341  frlmphl  20445  frlmup1  20462  nmparlem  23365  minveclem2  23536  lsatfixedN  35030  lfl0f  35090  lfladdcl  35092  lflnegcl  35096  lflvscl  35098  lkrlss  35116  lshpkrlem5  35135  lshpkrlem6  35136  dvh3dim2  37469  dvh3dim3N  37470  lcfrlem17  37580  lcfrlem19  37582  lcfrlem20  37583  lcfrlem23  37586  baerlem3lem1  37728  baerlem5alem1  37729  baerlem5blem1  37730  baerlem5alem2  37732  baerlem5blem2  37733  mapdindp0  37740  mapdindp2  37742  mapdindp4  37744  mapdh6lem2N  37755  mapdh6aN  37756  mapdh6dN  37760  mapdh6eN  37761  mapdh6hN  37764  hdmap1l6lem2  37829  hdmap1l6a  37830  hdmap1l6d  37834  hdmap1l6e  37835  hdmap1l6h  37838  hdmap11lem1  37862  hdmap11lem2  37863  hdmapneg  37867  hdmaprnlem3N  37871  hdmaprnlem3uN  37872  hdmaprnlem6N  37875  hdmaprnlem7N  37876  hdmaprnlem9N  37878  hdmaprnlem3eN  37879  hdmap14lem10  37898  hdmapinvlem3  37941  hdmapinvlem4  37942  hdmapglem7b  37949  hlhilphllem  37980  lincsumcl  43019