Theorem lmodvacl 20977

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  Grpcgrp 19001  LModclmod 20962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-grp 19004  df-lmod 20964

This theorem is referenced by:  lmodcom  21010  lmodvsghm  21025  lss1  21040  lspprabs  21197  lspabs2  21225  lspabs3  21226  lspfixed  21233  lspexch  21234  lspsolvlem  21247  ipdir  21770  ipdi  21771  ip2di  21772  ocvlss  21803  frlmphl  21912  frlmup1  21929  nmparlem  25379  minveclem2  25566  lsatfixedN  39761  lfl0f  39821  lfladdcl  39823  lflnegcl  39827  lflvscl  39829  lkrlss  39847  lshpkrlem5  39866  lshpkrlem6  39867  dvh3dim2  42200  dvh3dim3N  42201  lcfrlem17  42311  lcfrlem19  42313  lcfrlem20  42314  lcfrlem23  42317  baerlem3lem1  42459  baerlem5alem1  42460  baerlem5blem1  42461  baerlem5alem2  42463  baerlem5blem2  42464  mapdindp0  42471  mapdindp2  42473  mapdindp4  42475  mapdh6lem2N  42486  mapdh6aN  42487  mapdh6dN  42491  mapdh6eN  42492  mapdh6hN  42495  hdmap1l6lem2  42560  hdmap1l6a  42561  hdmap1l6d  42565  hdmap1l6e  42566  hdmap1l6h  42569  hdmap11lem1  42593  hdmap11lem2  42594  hdmapneg  42598  hdmaprnlem3N  42602  hdmaprnlem3uN  42603  hdmaprnlem6N  42606  hdmaprnlem7N  42607  hdmaprnlem9N  42609  hdmaprnlem3eN  42610  hdmap14lem10  42629  hdmapinvlem3  42672  hdmapinvlem4  42673  hdmapglem7b  42680  hlhilphllem  42711  frlmsnic  43288  lincsumcl  49188