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

Theorem lmodvacl 18643
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 18636 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 17196 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1350 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030   = wceq 1474  wcel 1976  cfv 5787  (class class class)co 6524  Basecbs 15638  +gcplusg 15711  Grpcgrp 17188  LModclmod 18629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-nul 4709
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-grp 17191  df-lmod 18631
This theorem is referenced by:  lmodcom  18675  lmodvsghm  18690  lss1  18703  lspprabs  18859  lspabs2  18884  lspabs3  18885  lspfixed  18892  lspexch  18893  lspsolvlem  18906  ipdir  19745  ipdi  19746  ip2di  19747  ocvlss  19774  frlmphl  19878  frlmup1  19895  nmparlem  22764  minveclem2  22919  lsatfixedN  33114  lfl0f  33174  lfladdcl  33176  lflnegcl  33180  lflvscl  33182  lkrlss  33200  lshpkrlem5  33219  lshpkrlem6  33220  dvh3dim2  35555  dvh3dim3N  35556  lcfrlem17  35666  lcfrlem19  35668  lcfrlem20  35669  lcfrlem23  35672  baerlem3lem1  35814  baerlem5alem1  35815  baerlem5blem1  35816  baerlem5alem2  35818  baerlem5blem2  35819  mapdindp0  35826  mapdindp2  35828  mapdindp4  35830  mapdh6lem2N  35841  mapdh6aN  35842  mapdh6dN  35846  mapdh6eN  35847  mapdh6hN  35850  hdmap1l6lem2  35916  hdmap1l6a  35917  hdmap1l6d  35921  hdmap1l6e  35922  hdmap1l6h  35925  hdmap11lem1  35951  hdmap11lem2  35952  hdmapneg  35956  hdmaprnlem3N  35960  hdmaprnlem3uN  35961  hdmaprnlem6N  35964  hdmaprnlem7N  35965  hdmaprnlem9N  35967  hdmaprnlem3eN  35968  hdmap14lem10  35987  hdmapinvlem3  36030  hdmapinvlem4  36031  hdmapglem7b  36038  hlhilphllem  36069  lincsumcl  42013
  Copyright terms: Public domain W3C validator