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

Theorem lmodvacl 20259
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 20252 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 18690 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1163 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087   = wceq 1541  wcel 2106  cfv 6491  (class class class)co 7349  Basecbs 17017  +gcplusg 17067  Grpcgrp 18682  LModclmod 20245
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 2708  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 2715  df-cleq 2729  df-clel 2815  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 6443  df-fv 6499  df-ov 7352  df-mgm 18431  df-sgrp 18480  df-mnd 18491  df-grp 18685  df-lmod 20247
This theorem is referenced by:  lmodcom  20291  lmodvsghm  20306  lss1  20322  lspprabs  20479  lspabs2  20504  lspabs3  20505  lspfixed  20512  lspexch  20513  lspsolvlem  20526  ipdir  20966  ipdi  20967  ip2di  20968  ocvlss  20999  frlmphl  21110  frlmup1  21127  nmparlem  24525  minveclem2  24712  lsatfixedN  37366  lfl0f  37426  lfladdcl  37428  lflnegcl  37432  lflvscl  37434  lkrlss  37452  lshpkrlem5  37471  lshpkrlem6  37472  dvh3dim2  39806  dvh3dim3N  39807  lcfrlem17  39917  lcfrlem19  39919  lcfrlem20  39920  lcfrlem23  39923  baerlem3lem1  40065  baerlem5alem1  40066  baerlem5blem1  40067  baerlem5alem2  40069  baerlem5blem2  40070  mapdindp0  40077  mapdindp2  40079  mapdindp4  40081  mapdh6lem2N  40092  mapdh6aN  40093  mapdh6dN  40097  mapdh6eN  40098  mapdh6hN  40101  hdmap1l6lem2  40166  hdmap1l6a  40167  hdmap1l6d  40171  hdmap1l6e  40172  hdmap1l6h  40175  hdmap11lem1  40199  hdmap11lem2  40200  hdmapneg  40204  hdmaprnlem3N  40208  hdmaprnlem3uN  40209  hdmaprnlem6N  40212  hdmaprnlem7N  40213  hdmaprnlem9N  40215  hdmaprnlem3eN  40216  hdmap14lem10  40235  hdmapinvlem3  40278  hdmapinvlem4  40279  hdmapglem7b  40286  hlhilphllem  40321  frlmsnic  40619  lincsumcl  46261
  Copyright terms: Public domain W3C validator