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

Theorem lmodvacl 19577
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 19570 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 18049 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1155 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079   = wceq 1528  wcel 2105  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  Grpcgrp 18041  LModclmod 19563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044  df-lmod 19565
This theorem is referenced by:  lmodcom  19609  lmodvsghm  19624  lss1  19639  lspprabs  19796  lspabs2  19821  lspabs3  19822  lspfixed  19829  lspexch  19830  lspsolvlem  19843  ipdir  20711  ipdi  20712  ip2di  20713  ocvlss  20744  frlmphl  20853  frlmup1  20870  nmparlem  23769  minveclem2  23956  lsatfixedN  36025  lfl0f  36085  lfladdcl  36087  lflnegcl  36091  lflvscl  36093  lkrlss  36111  lshpkrlem5  36130  lshpkrlem6  36131  dvh3dim2  38464  dvh3dim3N  38465  lcfrlem17  38575  lcfrlem19  38577  lcfrlem20  38578  lcfrlem23  38581  baerlem3lem1  38723  baerlem5alem1  38724  baerlem5blem1  38725  baerlem5alem2  38727  baerlem5blem2  38728  mapdindp0  38735  mapdindp2  38737  mapdindp4  38739  mapdh6lem2N  38750  mapdh6aN  38751  mapdh6dN  38755  mapdh6eN  38756  mapdh6hN  38759  hdmap1l6lem2  38824  hdmap1l6a  38825  hdmap1l6d  38829  hdmap1l6e  38830  hdmap1l6h  38833  hdmap11lem1  38857  hdmap11lem2  38858  hdmapneg  38862  hdmaprnlem3N  38866  hdmaprnlem3uN  38867  hdmaprnlem6N  38870  hdmaprnlem7N  38871  hdmaprnlem9N  38873  hdmaprnlem3eN  38874  hdmap14lem10  38893  hdmapinvlem3  38936  hdmapinvlem4  38937  hdmapglem7b  38944  hlhilphllem  38975  frlmsnic  39027  lincsumcl  44414
  Copyright terms: Public domain W3C validator