Theorem lmodvacl 20146

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  +_gcplusg 16971  Grpcgrp 18586  LModclmod 20132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-grp 18589  df-lmod 20134

This theorem is referenced by:  lmodcom  20178  lmodvsghm  20193  lss1  20209  lspprabs  20366  lspabs2  20391  lspabs3  20392  lspfixed  20399  lspexch  20400  lspsolvlem  20413  ipdir  20853  ipdi  20854  ip2di  20855  ocvlss  20886  frlmphl  20997  frlmup1  21014  nmparlem  24412  minveclem2  24599  lsatfixedN  37030  lfl0f  37090  lfladdcl  37092  lflnegcl  37096  lflvscl  37098  lkrlss  37116  lshpkrlem5  37135  lshpkrlem6  37136  dvh3dim2  39469  dvh3dim3N  39470  lcfrlem17  39580  lcfrlem19  39582  lcfrlem20  39583  lcfrlem23  39586  baerlem3lem1  39728  baerlem5alem1  39729  baerlem5blem1  39730  baerlem5alem2  39732  baerlem5blem2  39733  mapdindp0  39740  mapdindp2  39742  mapdindp4  39744  mapdh6lem2N  39755  mapdh6aN  39756  mapdh6dN  39760  mapdh6eN  39761  mapdh6hN  39764  hdmap1l6lem2  39829  hdmap1l6a  39830  hdmap1l6d  39834  hdmap1l6e  39835  hdmap1l6h  39838  hdmap11lem1  39862  hdmap11lem2  39863  hdmapneg  39867  hdmaprnlem3N  39871  hdmaprnlem3uN  39872  hdmaprnlem6N  39875  hdmaprnlem7N  39876  hdmaprnlem9N  39878  hdmaprnlem3eN  39879  hdmap14lem10  39898  hdmapinvlem3  39941  hdmapinvlem4  39942  hdmapglem7b  39949  hlhilphllem  39984  frlmsnic  40270  lincsumcl  45783