Theorem lmodvacl 20832

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  +_gcplusg 17271  Grpcgrp 18916  LModclmod 20817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-mgm 18618  df-sgrp 18697  df-mnd 18713  df-grp 18919  df-lmod 20819

This theorem is referenced by:  lmodcom  20865  lmodvsghm  20880  lss1  20895  lspprabs  21053  lspabs2  21081  lspabs3  21082  lspfixed  21089  lspexch  21090  lspsolvlem  21103  ipdir  21599  ipdi  21600  ip2di  21601  ocvlss  21632  frlmphl  21741  frlmup1  21758  nmparlem  25191  minveclem2  25378  lsatfixedN  39027  lfl0f  39087  lfladdcl  39089  lflnegcl  39093  lflvscl  39095  lkrlss  39113  lshpkrlem5  39132  lshpkrlem6  39133  dvh3dim2  41467  dvh3dim3N  41468  lcfrlem17  41578  lcfrlem19  41580  lcfrlem20  41581  lcfrlem23  41584  baerlem3lem1  41726  baerlem5alem1  41727  baerlem5blem1  41728  baerlem5alem2  41730  baerlem5blem2  41731  mapdindp0  41738  mapdindp2  41740  mapdindp4  41742  mapdh6lem2N  41753  mapdh6aN  41754  mapdh6dN  41758  mapdh6eN  41759  mapdh6hN  41762  hdmap1l6lem2  41827  hdmap1l6a  41828  hdmap1l6d  41832  hdmap1l6e  41833  hdmap1l6h  41836  hdmap11lem1  41860  hdmap11lem2  41861  hdmapneg  41865  hdmaprnlem3N  41869  hdmaprnlem3uN  41870  hdmaprnlem6N  41873  hdmaprnlem7N  41874  hdmaprnlem9N  41876  hdmaprnlem3eN  41877  hdmap14lem10  41896  hdmapinvlem3  41939  hdmapinvlem4  41940  hdmapglem7b  41947  hlhilphllem  41978  frlmsnic  42563  lincsumcl  48407