Theorem lmodvacl 19641

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  +_gcplusg 16557  Grpcgrp 18095  LModclmod 19627

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-grp 18098  df-lmod 19629

This theorem is referenced by:  lmodcom  19673  lmodvsghm  19688  lss1  19703  lspprabs  19860  lspabs2  19885  lspabs3  19886  lspfixed  19893  lspexch  19894  lspsolvlem  19907  ipdir  20328  ipdi  20329  ip2di  20330  ocvlss  20361  frlmphl  20470  frlmup1  20487  nmparlem  23843  minveclem2  24030  lsatfixedN  36305  lfl0f  36365  lfladdcl  36367  lflnegcl  36371  lflvscl  36373  lkrlss  36391  lshpkrlem5  36410  lshpkrlem6  36411  dvh3dim2  38744  dvh3dim3N  38745  lcfrlem17  38855  lcfrlem19  38857  lcfrlem20  38858  lcfrlem23  38861  baerlem3lem1  39003  baerlem5alem1  39004  baerlem5blem1  39005  baerlem5alem2  39007  baerlem5blem2  39008  mapdindp0  39015  mapdindp2  39017  mapdindp4  39019  mapdh6lem2N  39030  mapdh6aN  39031  mapdh6dN  39035  mapdh6eN  39036  mapdh6hN  39039  hdmap1l6lem2  39104  hdmap1l6a  39105  hdmap1l6d  39109  hdmap1l6e  39110  hdmap1l6h  39113  hdmap11lem1  39137  hdmap11lem2  39138  hdmapneg  39142  hdmaprnlem3N  39146  hdmaprnlem3uN  39147  hdmaprnlem6N  39150  hdmaprnlem7N  39151  hdmaprnlem9N  39153  hdmaprnlem3eN  39154  hdmap14lem10  39173  hdmapinvlem3  39216  hdmapinvlem4  39217  hdmapglem7b  39224  hlhilphllem  39255  frlmsnic  39453  lincsumcl  44840