Theorem lmodvacl 20810

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  +_gcplusg 17163  Grpcgrp 18848  LModclmod 20795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-mgm 18550  df-sgrp 18629  df-mnd 18645  df-grp 18851  df-lmod 20797

This theorem is referenced by:  lmodcom  20843  lmodvsghm  20858  lss1  20873  lspprabs  21031  lspabs2  21059  lspabs3  21060  lspfixed  21067  lspexch  21068  lspsolvlem  21081  ipdir  21578  ipdi  21579  ip2di  21580  ocvlss  21611  frlmphl  21720  frlmup1  21737  nmparlem  25167  minveclem2  25354  lsatfixedN  39129  lfl0f  39189  lfladdcl  39191  lflnegcl  39195  lflvscl  39197  lkrlss  39215  lshpkrlem5  39234  lshpkrlem6  39235  dvh3dim2  41568  dvh3dim3N  41569  lcfrlem17  41679  lcfrlem19  41681  lcfrlem20  41682  lcfrlem23  41685  baerlem3lem1  41827  baerlem5alem1  41828  baerlem5blem1  41829  baerlem5alem2  41831  baerlem5blem2  41832  mapdindp0  41839  mapdindp2  41841  mapdindp4  41843  mapdh6lem2N  41854  mapdh6aN  41855  mapdh6dN  41859  mapdh6eN  41860  mapdh6hN  41863  hdmap1l6lem2  41928  hdmap1l6a  41929  hdmap1l6d  41933  hdmap1l6e  41934  hdmap1l6h  41937  hdmap11lem1  41961  hdmap11lem2  41962  hdmapneg  41966  hdmaprnlem3N  41970  hdmaprnlem3uN  41971  hdmaprnlem6N  41974  hdmaprnlem7N  41975  hdmaprnlem9N  41977  hdmaprnlem3eN  41978  hdmap14lem10  41997  hdmapinvlem3  42040  hdmapinvlem4  42041  hdmapglem7b  42048  hlhilphllem  42079  frlmsnic  42659  lincsumcl  48557