MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvacl Structured version   Visualization version   GIF version

Theorem lmodvacl 19570
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
StepHypRef Expression
1 lmodgrp 19563 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 18043 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1157 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081   = wceq 1530  wcel 2106  cfv 6351  (class class class)co 7151  Basecbs 16475  +gcplusg 16557  Grpcgrp 18035  LModclmod 19556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-nul 5206
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-grp 18038  df-lmod 19558
This theorem is referenced by:  lmodcom  19602  lmodvsghm  19617  lss1  19632  lspprabs  19789  lspabs2  19814  lspabs3  19815  lspfixed  19822  lspexch  19823  lspsolvlem  19836  ipdir  20699  ipdi  20700  ip2di  20701  ocvlss  20732  frlmphl  20841  frlmup1  20858  nmparlem  23757  minveclem2  23944  lsatfixedN  36013  lfl0f  36073  lfladdcl  36075  lflnegcl  36079  lflvscl  36081  lkrlss  36099  lshpkrlem5  36118  lshpkrlem6  36119  dvh3dim2  38452  dvh3dim3N  38453  lcfrlem17  38563  lcfrlem19  38565  lcfrlem20  38566  lcfrlem23  38569  baerlem3lem1  38711  baerlem5alem1  38712  baerlem5blem1  38713  baerlem5alem2  38715  baerlem5blem2  38716  mapdindp0  38723  mapdindp2  38725  mapdindp4  38727  mapdh6lem2N  38738  mapdh6aN  38739  mapdh6dN  38743  mapdh6eN  38744  mapdh6hN  38747  hdmap1l6lem2  38812  hdmap1l6a  38813  hdmap1l6d  38817  hdmap1l6e  38818  hdmap1l6h  38821  hdmap11lem1  38845  hdmap11lem2  38846  hdmapneg  38850  hdmaprnlem3N  38854  hdmaprnlem3uN  38855  hdmaprnlem6N  38858  hdmaprnlem7N  38859  hdmaprnlem9N  38861  hdmaprnlem3eN  38862  hdmap14lem10  38881  hdmapinvlem3  38924  hdmapinvlem4  38925  hdmapglem7b  38932  hlhilphllem  38963  frlmsnic  39013  lincsumcl  44315
  Copyright terms: Public domain W3C validator