Theorem lmodvacl 20965

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  Grpcgrp 18990  LModclmod 20950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-grp 18993  df-lmod 20952

This theorem is referenced by:  lmodcom  20998  lmodvsghm  21013  lss1  21028  lspprabs  21185  lspabs2  21213  lspabs3  21214  lspfixed  21221  lspexch  21222  lspsolvlem  21235  ipdir  21749  ipdi  21750  ip2di  21751  ocvlss  21782  frlmphl  21891  frlmup1  21908  nmparlem  25359  minveclem2  25546  lsatfixedN  39645  lfl0f  39705  lfladdcl  39707  lflnegcl  39711  lflvscl  39713  lkrlss  39731  lshpkrlem5  39750  lshpkrlem6  39751  dvh3dim2  42084  dvh3dim3N  42085  lcfrlem17  42195  lcfrlem19  42197  lcfrlem20  42198  lcfrlem23  42201  baerlem3lem1  42343  baerlem5alem1  42344  baerlem5blem1  42345  baerlem5alem2  42347  baerlem5blem2  42348  mapdindp0  42355  mapdindp2  42357  mapdindp4  42359  mapdh6lem2N  42370  mapdh6aN  42371  mapdh6dN  42375  mapdh6eN  42376  mapdh6hN  42379  hdmap1l6lem2  42444  hdmap1l6a  42445  hdmap1l6d  42449  hdmap1l6e  42450  hdmap1l6h  42453  hdmap11lem1  42477  hdmap11lem2  42478  hdmapneg  42482  hdmaprnlem3N  42486  hdmaprnlem3uN  42487  hdmaprnlem6N  42490  hdmaprnlem7N  42491  hdmaprnlem9N  42493  hdmaprnlem3eN  42494  hdmap14lem10  42513  hdmapinvlem3  42556  hdmapinvlem4  42557  hdmapglem7b  42564  hlhilphllem  42595  frlmsnic  43170  lincsumcl  49062