Theorem lmodvacl 20922

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

Syntax hints:   → wi 4   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  +_gcplusg 17269  Grpcgrp 18958  LModclmod 20907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-mgm 18657  df-sgrp 18736  df-mnd 18752  df-grp 18961  df-lmod 20909

This theorem is referenced by:  lmodcom  20955  lmodvsghm  20970  lss1  20985  lspprabs  21142  lspabs2  21170  lspabs3  21171  lspfixed  21178  lspexch  21179  lspsolvlem  21192  ipdir  21671  ipdi  21672  ip2di  21673  ocvlss  21704  frlmphl  21813  frlmup1  21830  nmparlem  25281  minveclem2  25468  lsatfixedN  39597  lfl0f  39657  lfladdcl  39659  lflnegcl  39663  lflvscl  39665  lkrlss  39683  lshpkrlem5  39702  lshpkrlem6  39703  dvh3dim2  42036  dvh3dim3N  42037  lcfrlem17  42147  lcfrlem19  42149  lcfrlem20  42150  lcfrlem23  42153  baerlem3lem1  42295  baerlem5alem1  42296  baerlem5blem1  42297  baerlem5alem2  42299  baerlem5blem2  42300  mapdindp0  42307  mapdindp2  42309  mapdindp4  42311  mapdh6lem2N  42322  mapdh6aN  42323  mapdh6dN  42327  mapdh6eN  42328  mapdh6hN  42331  hdmap1l6lem2  42396  hdmap1l6a  42397  hdmap1l6d  42401  hdmap1l6e  42402  hdmap1l6h  42405  hdmap11lem1  42429  hdmap11lem2  42430  hdmapneg  42434  hdmaprnlem3N  42438  hdmaprnlem3uN  42439  hdmaprnlem6N  42442  hdmaprnlem7N  42443  hdmaprnlem9N  42445  hdmaprnlem3eN  42446  hdmap14lem10  42465  hdmapinvlem3  42508  hdmapinvlem4  42509  hdmapglem7b  42516  hlhilphllem  42547  frlmsnic  43122  lincsumcl  49017