Theorem lmodvacl 20890

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  +_gcplusg 17298  Grpcgrp 18964  LModclmod 20875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-grp 18967  df-lmod 20877

This theorem is referenced by:  lmodcom  20923  lmodvsghm  20938  lss1  20954  lspprabs  21112  lspabs2  21140  lspabs3  21141  lspfixed  21148  lspexch  21149  lspsolvlem  21162  ipdir  21675  ipdi  21676  ip2di  21677  ocvlss  21708  frlmphl  21819  frlmup1  21836  nmparlem  25287  minveclem2  25474  lsatfixedN  38991  lfl0f  39051  lfladdcl  39053  lflnegcl  39057  lflvscl  39059  lkrlss  39077  lshpkrlem5  39096  lshpkrlem6  39097  dvh3dim2  41431  dvh3dim3N  41432  lcfrlem17  41542  lcfrlem19  41544  lcfrlem20  41545  lcfrlem23  41548  baerlem3lem1  41690  baerlem5alem1  41691  baerlem5blem1  41692  baerlem5alem2  41694  baerlem5blem2  41695  mapdindp0  41702  mapdindp2  41704  mapdindp4  41706  mapdh6lem2N  41717  mapdh6aN  41718  mapdh6dN  41722  mapdh6eN  41723  mapdh6hN  41726  hdmap1l6lem2  41791  hdmap1l6a  41792  hdmap1l6d  41796  hdmap1l6e  41797  hdmap1l6h  41800  hdmap11lem1  41824  hdmap11lem2  41825  hdmapneg  41829  hdmaprnlem3N  41833  hdmaprnlem3uN  41834  hdmaprnlem6N  41837  hdmaprnlem7N  41838  hdmaprnlem9N  41840  hdmaprnlem3eN  41841  hdmap14lem10  41860  hdmapinvlem3  41903  hdmapinvlem4  41904  hdmapglem7b  41911  hlhilphllem  41946  frlmsnic  42527  lincsumcl  48277