Theorem lmodvacl 21180

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  Grpcgrp 19173  LModclmod 21165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176  df-lmod 21167

This theorem is used by:  lmodcom  21213  lmodvsghm  21228  lss1  21243  lspprabs  21400  lspabs2  21428  lspabs3  21429  lspfixed  21436  lspexch  21437  lspsolvlem  21450  ipdir  21975  ipdi  21976  ip2di  21977  ocvlss  22008  frlmphl  22117  frlmup1  22134  nmparlem  25590  minveclem2  25777  lsatfixedN  40258  lfl0f  40318  lfladdcl  40320  lflnegcl  40324  lflvscl  40326  lkrlss  40344  lshpkrlem5  40363  lshpkrlem6  40364  dvh3dim2  42697  dvh3dim3N  42698  lcfrlem17  42808  lcfrlem19  42810  lcfrlem20  42811  lcfrlem23  42814  baerlem3lem1  42956  baerlem5alem1  42957  baerlem5blem1  42958  baerlem5alem2  42960  baerlem5blem2  42961  mapdindp0  42968  mapdindp2  42970  mapdindp4  42972  mapdh6lem2N  42983  mapdh6aN  42984  mapdh6dN  42988  mapdh6eN  42989  mapdh6hN  42992  hdmap1l6lem2  43057  hdmap1l6a  43058  hdmap1l6d  43062  hdmap1l6e  43063  hdmap1l6h  43066  hdmap11lem1  43090  hdmap11lem2  43091  hdmapneg  43095  hdmaprnlem3N  43099  hdmaprnlem3uN  43100  hdmaprnlem6N  43103  hdmaprnlem7N  43104  hdmaprnlem9N  43106  hdmaprnlem3eN  43107  hdmap14lem10  43126  hdmapinvlem3  43169  hdmapinvlem4  43170  hdmapglem7b  43177  hlhilphllem  43208  frlmsnic  43797  lincsumcl  49748