Theorem lmodvacl 20838

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  Grpcgrp 18875  LModclmod 20823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878  df-lmod 20825

This theorem is referenced by:  lmodcom  20871  lmodvsghm  20886  lss1  20901  lspprabs  21059  lspabs2  21087  lspabs3  21088  lspfixed  21095  lspexch  21096  lspsolvlem  21109  ipdir  21606  ipdi  21607  ip2di  21608  ocvlss  21639  frlmphl  21748  frlmup1  21765  nmparlem  25207  minveclem2  25394  lsatfixedN  39379  lfl0f  39439  lfladdcl  39441  lflnegcl  39445  lflvscl  39447  lkrlss  39465  lshpkrlem5  39484  lshpkrlem6  39485  dvh3dim2  41818  dvh3dim3N  41819  lcfrlem17  41929  lcfrlem19  41931  lcfrlem20  41932  lcfrlem23  41935  baerlem3lem1  42077  baerlem5alem1  42078  baerlem5blem1  42079  baerlem5alem2  42081  baerlem5blem2  42082  mapdindp0  42089  mapdindp2  42091  mapdindp4  42093  mapdh6lem2N  42104  mapdh6aN  42105  mapdh6dN  42109  mapdh6eN  42110  mapdh6hN  42113  hdmap1l6lem2  42178  hdmap1l6a  42179  hdmap1l6d  42183  hdmap1l6e  42184  hdmap1l6h  42187  hdmap11lem1  42211  hdmap11lem2  42212  hdmapneg  42216  hdmaprnlem3N  42220  hdmaprnlem3uN  42221  hdmaprnlem6N  42224  hdmaprnlem7N  42225  hdmaprnlem9N  42227  hdmaprnlem3eN  42228  hdmap14lem10  42247  hdmapinvlem3  42290  hdmapinvlem4  42291  hdmapglem7b  42298  hlhilphllem  42329  frlmsnic  42904  lincsumcl  48785