Theorem lmodvacl 21130

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6531  (class class class)co 7412  Basecbs 17367  +_gcplusg 17408  Grpcgrp 19124  LModclmod 21115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-grp 19127  df-lmod 21117

This theorem is used by:  lmodcom  21163  lmodvsghm  21178  lss1  21193  lspprabs  21350  lspabs2  21378  lspabs3  21379  lspfixed  21386  lspexch  21387  lspsolvlem  21400  ipdir  21925  ipdi  21926  ip2di  21927  ocvlss  21958  frlmphl  22067  frlmup1  22084  nmparlem  25540  minveclem2  25727  lsatfixedN  40034  lfl0f  40094  lfladdcl  40096  lflnegcl  40100  lflvscl  40102  lkrlss  40120  lshpkrlem5  40139  lshpkrlem6  40140  dvh3dim2  42473  dvh3dim3N  42474  lcfrlem17  42584  lcfrlem19  42586  lcfrlem20  42587  lcfrlem23  42590  baerlem3lem1  42732  baerlem5alem1  42733  baerlem5blem1  42734  baerlem5alem2  42736  baerlem5blem2  42737  mapdindp0  42744  mapdindp2  42746  mapdindp4  42748  mapdh6lem2N  42759  mapdh6aN  42760  mapdh6dN  42764  mapdh6eN  42765  mapdh6hN  42768  hdmap1l6lem2  42833  hdmap1l6a  42834  hdmap1l6d  42838  hdmap1l6e  42839  hdmap1l6h  42842  hdmap11lem1  42866  hdmap11lem2  42867  hdmapneg  42871  hdmaprnlem3N  42875  hdmaprnlem3uN  42876  hdmaprnlem6N  42879  hdmaprnlem7N  42880  hdmaprnlem9N  42882  hdmaprnlem3eN  42883  hdmap14lem10  42902  hdmapinvlem3  42945  hdmapinvlem4  42946  hdmapglem7b  42953  hlhilphllem  42984  frlmsnic  43566  lincsumcl  49487