Theorem lmodvacl 20796

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  Grpcgrp 18830  LModclmod 20781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-grp 18833  df-lmod 20783

This theorem is referenced by:  lmodcom  20829  lmodvsghm  20844  lss1  20859  lspprabs  21017  lspabs2  21045  lspabs3  21046  lspfixed  21053  lspexch  21054  lspsolvlem  21067  ipdir  21564  ipdi  21565  ip2di  21566  ocvlss  21597  frlmphl  21706  frlmup1  21723  nmparlem  25155  minveclem2  25342  lsatfixedN  38987  lfl0f  39047  lfladdcl  39049  lflnegcl  39053  lflvscl  39055  lkrlss  39073  lshpkrlem5  39092  lshpkrlem6  39093  dvh3dim2  41427  dvh3dim3N  41428  lcfrlem17  41538  lcfrlem19  41540  lcfrlem20  41541  lcfrlem23  41544  baerlem3lem1  41686  baerlem5alem1  41687  baerlem5blem1  41688  baerlem5alem2  41690  baerlem5blem2  41691  mapdindp0  41698  mapdindp2  41700  mapdindp4  41702  mapdh6lem2N  41713  mapdh6aN  41714  mapdh6dN  41718  mapdh6eN  41719  mapdh6hN  41722  hdmap1l6lem2  41787  hdmap1l6a  41788  hdmap1l6d  41792  hdmap1l6e  41793  hdmap1l6h  41796  hdmap11lem1  41820  hdmap11lem2  41821  hdmapneg  41825  hdmaprnlem3N  41829  hdmaprnlem3uN  41830  hdmaprnlem6N  41833  hdmaprnlem7N  41834  hdmaprnlem9N  41836  hdmaprnlem3eN  41837  hdmap14lem10  41856  hdmapinvlem3  41899  hdmapinvlem4  41900  hdmapglem7b  41907  hlhilphllem  41938  frlmsnic  42513  lincsumcl  48417