Theorem lmodvacl 20895

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

Step	Hyp	Ref	Expression
1		lmodgrp 20887	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		lmodvacl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lmodvacl.a	. . 3 ⊢ + = (+g‘𝑊)
4	2, 3	grpcl 18981	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
5	1, 4	syl3an1 1163	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  Grpcgrp 18973  LModclmod 20880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-lmod 20882

This theorem is referenced by:  lmodcom  20928  lmodvsghm  20943  lss1  20959  lspprabs  21117  lspabs2  21145  lspabs3  21146  lspfixed  21153  lspexch  21154  lspsolvlem  21167  ipdir  21680  ipdi  21681  ip2di  21682  ocvlss  21713  frlmphl  21824  frlmup1  21841  nmparlem  25292  minveclem2  25479  lsatfixedN  38965  lfl0f  39025  lfladdcl  39027  lflnegcl  39031  lflvscl  39033  lkrlss  39051  lshpkrlem5  39070  lshpkrlem6  39071  dvh3dim2  41405  dvh3dim3N  41406  lcfrlem17  41516  lcfrlem19  41518  lcfrlem20  41519  lcfrlem23  41522  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem5alem2  41668  baerlem5blem2  41669  mapdindp0  41676  mapdindp2  41678  mapdindp4  41680  mapdh6lem2N  41691  mapdh6aN  41692  mapdh6dN  41696  mapdh6eN  41697  mapdh6hN  41700  hdmap1l6lem2  41765  hdmap1l6a  41766  hdmap1l6d  41770  hdmap1l6e  41771  hdmap1l6h  41774  hdmap11lem1  41798  hdmap11lem2  41799  hdmapneg  41803  hdmaprnlem3N  41807  hdmaprnlem3uN  41808  hdmaprnlem6N  41811  hdmaprnlem7N  41812  hdmaprnlem9N  41814  hdmaprnlem3eN  41815  hdmap14lem10  41834  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem7b  41885  hlhilphllem  41920  frlmsnic  42495  lincsumcl  48160