Theorem lmodvacl 20052

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  Grpcgrp 18492  LModclmod 20038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495  df-lmod 20040

This theorem is referenced by:  lmodcom  20084  lmodvsghm  20099  lss1  20115  lspprabs  20272  lspabs2  20297  lspabs3  20298  lspfixed  20305  lspexch  20306  lspsolvlem  20319  ipdir  20756  ipdi  20757  ip2di  20758  ocvlss  20789  frlmphl  20898  frlmup1  20915  nmparlem  24308  minveclem2  24495  lsatfixedN  36950  lfl0f  37010  lfladdcl  37012  lflnegcl  37016  lflvscl  37018  lkrlss  37036  lshpkrlem5  37055  lshpkrlem6  37056  dvh3dim2  39389  dvh3dim3N  39390  lcfrlem17  39500  lcfrlem19  39502  lcfrlem20  39503  lcfrlem23  39506  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  baerlem5alem2  39652  baerlem5blem2  39653  mapdindp0  39660  mapdindp2  39662  mapdindp4  39664  mapdh6lem2N  39675  mapdh6aN  39676  mapdh6dN  39680  mapdh6eN  39681  mapdh6hN  39684  hdmap1l6lem2  39749  hdmap1l6a  39750  hdmap1l6d  39754  hdmap1l6e  39755  hdmap1l6h  39758  hdmap11lem1  39782  hdmap11lem2  39783  hdmapneg  39787  hdmaprnlem3N  39791  hdmaprnlem3uN  39792  hdmaprnlem6N  39795  hdmaprnlem7N  39796  hdmaprnlem9N  39798  hdmaprnlem3eN  39799  hdmap14lem10  39818  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem7b  39869  hlhilphllem  39904  frlmsnic  40188  lincsumcl  45660