Theorem lmodvacl 20873

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  Grpcgrp 18951  LModclmod 20858

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 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-lmod 20860

This theorem is referenced by:  lmodcom  20906  lmodvsghm  20921  lss1  20936  lspprabs  21094  lspabs2  21122  lspabs3  21123  lspfixed  21130  lspexch  21131  lspsolvlem  21144  ipdir  21657  ipdi  21658  ip2di  21659  ocvlss  21690  frlmphl  21801  frlmup1  21818  nmparlem  25273  minveclem2  25460  lsatfixedN  39010  lfl0f  39070  lfladdcl  39072  lflnegcl  39076  lflvscl  39078  lkrlss  39096  lshpkrlem5  39115  lshpkrlem6  39116  dvh3dim2  41450  dvh3dim3N  41451  lcfrlem17  41561  lcfrlem19  41563  lcfrlem20  41564  lcfrlem23  41567  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  baerlem5alem2  41713  baerlem5blem2  41714  mapdindp0  41721  mapdindp2  41723  mapdindp4  41725  mapdh6lem2N  41736  mapdh6aN  41737  mapdh6dN  41741  mapdh6eN  41742  mapdh6hN  41745  hdmap1l6lem2  41810  hdmap1l6a  41811  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6h  41819  hdmap11lem1  41843  hdmap11lem2  41844  hdmapneg  41848  hdmaprnlem3N  41852  hdmaprnlem3uN  41853  hdmaprnlem6N  41856  hdmaprnlem7N  41857  hdmaprnlem9N  41859  hdmaprnlem3eN  41860  hdmap14lem10  41879  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem7b  41930  hlhilphllem  41965  frlmsnic  42550  lincsumcl  48348