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

Theorem lmodvacl 20283
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 20276 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 18710 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1163 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087   = wceq 1541  wcel 2106  cfv 6493  (class class class)co 7351  Basecbs 17037  +gcplusg 17087  Grpcgrp 18702  LModclmod 20269
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 2707  ax-nul 5261
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 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6445  df-fv 6501  df-ov 7354  df-mgm 18451  df-sgrp 18500  df-mnd 18511  df-grp 18705  df-lmod 20271
This theorem is referenced by:  lmodcom  20315  lmodvsghm  20330  lss1  20346  lspprabs  20503  lspabs2  20528  lspabs3  20529  lspfixed  20536  lspexch  20537  lspsolvlem  20550  ipdir  20990  ipdi  20991  ip2di  20992  ocvlss  21023  frlmphl  21134  frlmup1  21151  nmparlem  24549  minveclem2  24736  lsatfixedN  37403  lfl0f  37463  lfladdcl  37465  lflnegcl  37469  lflvscl  37471  lkrlss  37489  lshpkrlem5  37508  lshpkrlem6  37509  dvh3dim2  39843  dvh3dim3N  39844  lcfrlem17  39954  lcfrlem19  39956  lcfrlem20  39957  lcfrlem23  39960  baerlem3lem1  40102  baerlem5alem1  40103  baerlem5blem1  40104  baerlem5alem2  40106  baerlem5blem2  40107  mapdindp0  40114  mapdindp2  40116  mapdindp4  40118  mapdh6lem2N  40129  mapdh6aN  40130  mapdh6dN  40134  mapdh6eN  40135  mapdh6hN  40138  hdmap1l6lem2  40203  hdmap1l6a  40204  hdmap1l6d  40208  hdmap1l6e  40209  hdmap1l6h  40212  hdmap11lem1  40236  hdmap11lem2  40237  hdmapneg  40241  hdmaprnlem3N  40245  hdmaprnlem3uN  40246  hdmaprnlem6N  40249  hdmaprnlem7N  40250  hdmaprnlem9N  40252  hdmaprnlem3eN  40253  hdmap14lem10  40272  hdmapinvlem3  40315  hdmapinvlem4  40316  hdmapglem7b  40323  hlhilphllem  40358  frlmsnic  40654  lincsumcl  46407
  Copyright terms: Public domain W3C validator