Theorem lmodvacl 19721

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ‘cfv 6339  (class class class)co 7155  Basecbs 16546  +_gcplusg 16628  Grpcgrp 18174  LModclmod 19707

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-nul 5179

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-iota 6298  df-fv 6347  df-ov 7158  df-mgm 17923  df-sgrp 17972  df-mnd 17983  df-grp 18177  df-lmod 19709

This theorem is referenced by:  lmodcom  19753  lmodvsghm  19768  lss1  19783  lspprabs  19940  lspabs2  19965  lspabs3  19966  lspfixed  19973  lspexch  19974  lspsolvlem  19987  ipdir  20409  ipdi  20410  ip2di  20411  ocvlss  20442  frlmphl  20551  frlmup1  20568  nmparlem  23944  minveclem2  24131  lsatfixedN  36611  lfl0f  36671  lfladdcl  36673  lflnegcl  36677  lflvscl  36679  lkrlss  36697  lshpkrlem5  36716  lshpkrlem6  36717  dvh3dim2  39050  dvh3dim3N  39051  lcfrlem17  39161  lcfrlem19  39163  lcfrlem20  39164  lcfrlem23  39167  baerlem3lem1  39309  baerlem5alem1  39310  baerlem5blem1  39311  baerlem5alem2  39313  baerlem5blem2  39314  mapdindp0  39321  mapdindp2  39323  mapdindp4  39325  mapdh6lem2N  39336  mapdh6aN  39337  mapdh6dN  39341  mapdh6eN  39342  mapdh6hN  39345  hdmap1l6lem2  39410  hdmap1l6a  39411  hdmap1l6d  39415  hdmap1l6e  39416  hdmap1l6h  39419  hdmap11lem1  39443  hdmap11lem2  39444  hdmapneg  39448  hdmaprnlem3N  39452  hdmaprnlem3uN  39453  hdmaprnlem6N  39456  hdmaprnlem7N  39457  hdmaprnlem9N  39459  hdmaprnlem3eN  39460  hdmap14lem10  39479  hdmapinvlem3  39522  hdmapinvlem4  39523  hdmapglem7b  39530  hlhilphllem  39561  frlmsnic  39798  lincsumcl  45233