Theorem lmodvacl 20826

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 20818	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		lmodvacl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lmodvacl.a	. . 3 ⊢ + = (+g‘𝑊)
4	2, 3	grpcl 18871	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
5	1, 4	syl3an1 1163	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  Grpcgrp 18863  LModclmod 20811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18866  df-lmod 20813

This theorem is referenced by:  lmodcom  20859  lmodvsghm  20874  lss1  20889  lspprabs  21047  lspabs2  21075  lspabs3  21076  lspfixed  21083  lspexch  21084  lspsolvlem  21097  ipdir  21594  ipdi  21595  ip2di  21596  ocvlss  21627  frlmphl  21736  frlmup1  21753  nmparlem  25195  minveclem2  25382  lsatfixedN  39265  lfl0f  39325  lfladdcl  39327  lflnegcl  39331  lflvscl  39333  lkrlss  39351  lshpkrlem5  39370  lshpkrlem6  39371  dvh3dim2  41704  dvh3dim3N  41705  lcfrlem17  41815  lcfrlem19  41817  lcfrlem20  41818  lcfrlem23  41821  baerlem3lem1  41963  baerlem5alem1  41964  baerlem5blem1  41965  baerlem5alem2  41967  baerlem5blem2  41968  mapdindp0  41975  mapdindp2  41977  mapdindp4  41979  mapdh6lem2N  41990  mapdh6aN  41991  mapdh6dN  41995  mapdh6eN  41996  mapdh6hN  41999  hdmap1l6lem2  42064  hdmap1l6a  42065  hdmap1l6d  42069  hdmap1l6e  42070  hdmap1l6h  42073  hdmap11lem1  42097  hdmap11lem2  42098  hdmapneg  42102  hdmaprnlem3N  42106  hdmaprnlem3uN  42107  hdmaprnlem6N  42110  hdmaprnlem7N  42111  hdmaprnlem9N  42113  hdmaprnlem3eN  42114  hdmap14lem10  42133  hdmapinvlem3  42176  hdmapinvlem4  42177  hdmapglem7b  42184  hlhilphllem  42215  frlmsnic  42791  lincsumcl  48673