Theorem lmodvacl 21065

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  Grpcgrp 19063  LModclmod 21050

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-grp 19066  df-lmod 21052

This theorem is used by:  lmodcom  21098  lmodvsghm  21113  lss1  21128  lspprabs  21285  lspabs2  21313  lspabs3  21314  lspfixed  21321  lspexch  21322  lspsolvlem  21335  ipdir  21858  ipdi  21859  ip2di  21860  ocvlss  21891  frlmphl  22000  frlmup1  22017  nmparlem  25473  minveclem2  25660  lsatfixedN  39890  lfl0f  39950  lfladdcl  39952  lflnegcl  39956  lflvscl  39958  lkrlss  39976  lshpkrlem5  39995  lshpkrlem6  39996  dvh3dim2  42329  dvh3dim3N  42330  lcfrlem17  42440  lcfrlem19  42442  lcfrlem20  42443  lcfrlem23  42446  baerlem3lem1  42588  baerlem5alem1  42589  baerlem5blem1  42590  baerlem5alem2  42592  baerlem5blem2  42593  mapdindp0  42600  mapdindp2  42602  mapdindp4  42604  mapdh6lem2N  42615  mapdh6aN  42616  mapdh6dN  42620  mapdh6eN  42621  mapdh6hN  42624  hdmap1l6lem2  42689  hdmap1l6a  42690  hdmap1l6d  42694  hdmap1l6e  42695  hdmap1l6h  42698  hdmap11lem1  42722  hdmap11lem2  42723  hdmapneg  42727  hdmaprnlem3N  42731  hdmaprnlem3uN  42732  hdmaprnlem6N  42735  hdmaprnlem7N  42736  hdmaprnlem9N  42738  hdmaprnlem3eN  42739  hdmap14lem10  42758  hdmapinvlem3  42801  hdmapinvlem4  42802  hdmapglem7b  42809  hlhilphllem  42840  frlmsnic  43430  lincsumcl  49369