Theorem lmodvacl 20861

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  Grpcgrp 18900  LModclmod 20846

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 5241

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-lmod 20848

This theorem is referenced by:  lmodcom  20894  lmodvsghm  20909  lss1  20924  lspprabs  21082  lspabs2  21110  lspabs3  21111  lspfixed  21118  lspexch  21119  lspsolvlem  21132  ipdir  21629  ipdi  21630  ip2di  21631  ocvlss  21662  frlmphl  21771  frlmup1  21788  nmparlem  25216  minveclem2  25403  lsatfixedN  39469  lfl0f  39529  lfladdcl  39531  lflnegcl  39535  lflvscl  39537  lkrlss  39555  lshpkrlem5  39574  lshpkrlem6  39575  dvh3dim2  41908  dvh3dim3N  41909  lcfrlem17  42019  lcfrlem19  42021  lcfrlem20  42022  lcfrlem23  42025  baerlem3lem1  42167  baerlem5alem1  42168  baerlem5blem1  42169  baerlem5alem2  42171  baerlem5blem2  42172  mapdindp0  42179  mapdindp2  42181  mapdindp4  42183  mapdh6lem2N  42194  mapdh6aN  42195  mapdh6dN  42199  mapdh6eN  42200  mapdh6hN  42203  hdmap1l6lem2  42268  hdmap1l6a  42269  hdmap1l6d  42273  hdmap1l6e  42274  hdmap1l6h  42277  hdmap11lem1  42301  hdmap11lem2  42302  hdmapneg  42306  hdmaprnlem3N  42310  hdmaprnlem3uN  42311  hdmaprnlem6N  42314  hdmaprnlem7N  42315  hdmaprnlem9N  42317  hdmaprnlem3eN  42318  hdmap14lem10  42337  hdmapinvlem3  42380  hdmapinvlem4  42381  hdmapglem7b  42388  hlhilphllem  42419  frlmsnic  42999  lincsumcl  48919