Theorem lmodvacl 20490

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6543  (class class class)co 7411  Basecbs 17146  +_gcplusg 17199  Grpcgrp 18821  LModclmod 20475

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-grp 18824  df-lmod 20477

This theorem is referenced by:  lmodcom  20523  lmodvsghm  20538  lss1  20554  lspprabs  20711  lspabs2  20739  lspabs3  20740  lspfixed  20747  lspexch  20748  lspsolvlem  20761  ipdir  21198  ipdi  21199  ip2di  21200  ocvlss  21231  frlmphl  21342  frlmup1  21359  nmparlem  24763  minveclem2  24950  lsatfixedN  37965  lfl0f  38025  lfladdcl  38027  lflnegcl  38031  lflvscl  38033  lkrlss  38051  lshpkrlem5  38070  lshpkrlem6  38071  dvh3dim2  40405  dvh3dim3N  40406  lcfrlem17  40516  lcfrlem19  40518  lcfrlem20  40519  lcfrlem23  40522  baerlem3lem1  40664  baerlem5alem1  40665  baerlem5blem1  40666  baerlem5alem2  40668  baerlem5blem2  40669  mapdindp0  40676  mapdindp2  40678  mapdindp4  40680  mapdh6lem2N  40691  mapdh6aN  40692  mapdh6dN  40696  mapdh6eN  40697  mapdh6hN  40700  hdmap1l6lem2  40765  hdmap1l6a  40766  hdmap1l6d  40770  hdmap1l6e  40771  hdmap1l6h  40774  hdmap11lem1  40798  hdmap11lem2  40799  hdmapneg  40803  hdmaprnlem3N  40807  hdmaprnlem3uN  40808  hdmaprnlem6N  40811  hdmaprnlem7N  40812  hdmaprnlem9N  40814  hdmaprnlem3eN  40815  hdmap14lem10  40834  hdmapinvlem3  40877  hdmapinvlem4  40878  hdmapglem7b  40885  hlhilphllem  40920  frlmsnic  41192  lincsumcl  47190