Theorem lmodvacl 21033

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  +_gcplusg 17335  Grpcgrp 19031  LModclmod 21018

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-mgm 18723  df-sgrp 18806  df-mnd 18822  df-grp 19034  df-lmod 21020

This theorem is used by:  lmodcom  21066  lmodvsghm  21081  lss1  21096  lspprabs  21253  lspabs2  21281  lspabs3  21282  lspfixed  21289  lspexch  21290  lspsolvlem  21303  ipdir  21826  ipdi  21827  ip2di  21828  ocvlss  21859  frlmphl  21968  frlmup1  21985  nmparlem  25435  minveclem2  25622  lsatfixedN  39824  lfl0f  39884  lfladdcl  39886  lflnegcl  39890  lflvscl  39892  lkrlss  39910  lshpkrlem5  39929  lshpkrlem6  39930  dvh3dim2  42263  dvh3dim3N  42264  lcfrlem17  42374  lcfrlem19  42376  lcfrlem20  42377  lcfrlem23  42380  baerlem3lem1  42522  baerlem5alem1  42523  baerlem5blem1  42524  baerlem5alem2  42526  baerlem5blem2  42527  mapdindp0  42534  mapdindp2  42536  mapdindp4  42538  mapdh6lem2N  42549  mapdh6aN  42550  mapdh6dN  42554  mapdh6eN  42555  mapdh6hN  42558  hdmap1l6lem2  42623  hdmap1l6a  42624  hdmap1l6d  42628  hdmap1l6e  42629  hdmap1l6h  42632  hdmap11lem1  42656  hdmap11lem2  42657  hdmapneg  42661  hdmaprnlem3N  42665  hdmaprnlem3uN  42666  hdmaprnlem6N  42669  hdmaprnlem7N  42670  hdmaprnlem9N  42672  hdmaprnlem3eN  42673  hdmap14lem10  42692  hdmapinvlem3  42735  hdmapinvlem4  42736  hdmapglem7b  42743  hlhilphllem  42774  frlmsnic  43349  lincsumcl  49252