Theorem lmodvacl 20828

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  (class class class)co 7358  Basecbs 17137  +_gcplusg 17178  Grpcgrp 18867  LModclmod 20813

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-grp 18870  df-lmod 20815

This theorem is referenced by:  lmodcom  20861  lmodvsghm  20876  lss1  20891  lspprabs  21049  lspabs2  21077  lspabs3  21078  lspfixed  21085  lspexch  21086  lspsolvlem  21099  ipdir  21596  ipdi  21597  ip2di  21598  ocvlss  21629  frlmphl  21738  frlmup1  21755  nmparlem  25184  minveclem2  25371  lsatfixedN  39446  lfl0f  39506  lfladdcl  39508  lflnegcl  39512  lflvscl  39514  lkrlss  39532  lshpkrlem5  39551  lshpkrlem6  39552  dvh3dim2  41885  dvh3dim3N  41886  lcfrlem17  41996  lcfrlem19  41998  lcfrlem20  41999  lcfrlem23  42002  baerlem3lem1  42144  baerlem5alem1  42145  baerlem5blem1  42146  baerlem5alem2  42148  baerlem5blem2  42149  mapdindp0  42156  mapdindp2  42158  mapdindp4  42160  mapdh6lem2N  42171  mapdh6aN  42172  mapdh6dN  42176  mapdh6eN  42177  mapdh6hN  42180  hdmap1l6lem2  42245  hdmap1l6a  42246  hdmap1l6d  42250  hdmap1l6e  42251  hdmap1l6h  42254  hdmap11lem1  42278  hdmap11lem2  42279  hdmapneg  42283  hdmaprnlem3N  42287  hdmaprnlem3uN  42288  hdmaprnlem6N  42291  hdmaprnlem7N  42292  hdmaprnlem9N  42294  hdmaprnlem3eN  42295  hdmap14lem10  42314  hdmapinvlem3  42357  hdmapinvlem4  42358  hdmapglem7b  42365  hlhilphllem  42396  frlmsnic  42984  lincsumcl  48865