Theorem lmodvacl 20393

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  +_gcplusg 17147  Grpcgrp 18762  LModclmod 20378

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 2702  ax-nul 5268

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 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-grp 18765  df-lmod 20380

This theorem is referenced by:  lmodcom  20425  lmodvsghm  20440  lss1  20456  lspprabs  20613  lspabs2  20640  lspabs3  20641  lspfixed  20648  lspexch  20649  lspsolvlem  20662  ipdir  21080  ipdi  21081  ip2di  21082  ocvlss  21113  frlmphl  21224  frlmup1  21241  nmparlem  24640  minveclem2  24827  lsatfixedN  37544  lfl0f  37604  lfladdcl  37606  lflnegcl  37610  lflvscl  37612  lkrlss  37630  lshpkrlem5  37649  lshpkrlem6  37650  dvh3dim2  39984  dvh3dim3N  39985  lcfrlem17  40095  lcfrlem19  40097  lcfrlem20  40098  lcfrlem23  40101  baerlem3lem1  40243  baerlem5alem1  40244  baerlem5blem1  40245  baerlem5alem2  40247  baerlem5blem2  40248  mapdindp0  40255  mapdindp2  40257  mapdindp4  40259  mapdh6lem2N  40270  mapdh6aN  40271  mapdh6dN  40275  mapdh6eN  40276  mapdh6hN  40279  hdmap1l6lem2  40344  hdmap1l6a  40345  hdmap1l6d  40349  hdmap1l6e  40350  hdmap1l6h  40353  hdmap11lem1  40377  hdmap11lem2  40378  hdmapneg  40382  hdmaprnlem3N  40386  hdmaprnlem3uN  40387  hdmaprnlem6N  40390  hdmaprnlem7N  40391  hdmaprnlem9N  40393  hdmaprnlem3eN  40394  hdmap14lem10  40413  hdmapinvlem3  40456  hdmapinvlem4  40457  hdmapglem7b  40464  hlhilphllem  40499  frlmsnic  40786  lincsumcl  46632