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 18691 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1164 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  cfv 6492  (class class class)co 7350  Basecbs 17018  +gcplusg 17068  Grpcgrp 18683  LModclmod 20245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-nul 5262
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-mgm 18432  df-sgrp 18481  df-mnd 18492  df-grp 18686  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  37357  lfl0f  37417  lfladdcl  37419  lflnegcl  37423  lflvscl  37425  lkrlss  37443  lshpkrlem5  37462  lshpkrlem6  37463  dvh3dim2  39797  dvh3dim3N  39798  lcfrlem17  39908  lcfrlem19  39910  lcfrlem20  39911  lcfrlem23  39914  baerlem3lem1  40056  baerlem5alem1  40057  baerlem5blem1  40058  baerlem5alem2  40060  baerlem5blem2  40061  mapdindp0  40068  mapdindp2  40070  mapdindp4  40072  mapdh6lem2N  40083  mapdh6aN  40084  mapdh6dN  40088  mapdh6eN  40089  mapdh6hN  40092  hdmap1l6lem2  40157  hdmap1l6a  40158  hdmap1l6d  40162  hdmap1l6e  40163  hdmap1l6h  40166  hdmap11lem1  40190  hdmap11lem2  40191  hdmapneg  40195  hdmaprnlem3N  40199  hdmaprnlem3uN  40200  hdmaprnlem6N  40203  hdmaprnlem7N  40204  hdmaprnlem9N  40206  hdmaprnlem3eN  40207  hdmap14lem10  40226  hdmapinvlem3  40269  hdmapinvlem4  40270  hdmapglem7b  40277  hlhilphllem  40312  frlmsnic  40598  lincsumcl  46212
  Copyright terms: Public domain W3C validator