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

Theorem lmodvacl 18817
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 18810 . 2 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2 lmodvacl.v . . 3 𝑉 = (Base‘𝑊)
3 lmodvacl.a . . 3 + = (+g𝑊)
42, 3grpcl 17370 . 2 ((𝑊 ∈ Grp ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
51, 4syl3an1 1356 1 ((𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  cfv 5857  (class class class)co 6615  Basecbs 15800  +gcplusg 15881  Grpcgrp 17362  LModclmod 18803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-grp 17365  df-lmod 18805
This theorem is referenced by:  lmodcom  18849  lmodvsghm  18864  lss1  18879  lspprabs  19035  lspabs2  19060  lspabs3  19061  lspfixed  19068  lspexch  19069  lspsolvlem  19082  ipdir  19924  ipdi  19925  ip2di  19926  ocvlss  19956  frlmphl  20060  frlmup1  20077  nmparlem  22978  minveclem2  23137  lsatfixedN  33815  lfl0f  33875  lfladdcl  33877  lflnegcl  33881  lflvscl  33883  lkrlss  33901  lshpkrlem5  33920  lshpkrlem6  33921  dvh3dim2  36256  dvh3dim3N  36257  lcfrlem17  36367  lcfrlem19  36369  lcfrlem20  36370  lcfrlem23  36373  baerlem3lem1  36515  baerlem5alem1  36516  baerlem5blem1  36517  baerlem5alem2  36519  baerlem5blem2  36520  mapdindp0  36527  mapdindp2  36529  mapdindp4  36531  mapdh6lem2N  36542  mapdh6aN  36543  mapdh6dN  36547  mapdh6eN  36548  mapdh6hN  36551  hdmap1l6lem2  36617  hdmap1l6a  36618  hdmap1l6d  36622  hdmap1l6e  36623  hdmap1l6h  36626  hdmap11lem1  36652  hdmap11lem2  36653  hdmapneg  36657  hdmaprnlem3N  36661  hdmaprnlem3uN  36662  hdmaprnlem6N  36665  hdmaprnlem7N  36666  hdmaprnlem9N  36668  hdmaprnlem3eN  36669  hdmap14lem10  36688  hdmapinvlem3  36731  hdmapinvlem4  36732  hdmapglem7b  36739  hlhilphllem  36770  lincsumcl  41538
  Copyright terms: Public domain W3C validator