Theorem lmodvacl 21155

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  +_gcplusg 17433  Grpcgrp 19149  LModclmod 21140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-grp 19152  df-lmod 21142

This theorem is used by:  lmodcom  21188  lmodvsghm  21203  lss1  21218  lspprabs  21375  lspabs2  21403  lspabs3  21404  lspfixed  21411  lspexch  21412  lspsolvlem  21425  ipdir  21950  ipdi  21951  ip2di  21952  ocvlss  21983  frlmphl  22092  frlmup1  22109  nmparlem  25565  minveclem2  25752  lsatfixedN  40159  lfl0f  40219  lfladdcl  40221  lflnegcl  40225  lflvscl  40227  lkrlss  40245  lshpkrlem5  40264  lshpkrlem6  40265  dvh3dim2  42598  dvh3dim3N  42599  lcfrlem17  42709  lcfrlem19  42711  lcfrlem20  42712  lcfrlem23  42715  baerlem3lem1  42857  baerlem5alem1  42858  baerlem5blem1  42859  baerlem5alem2  42861  baerlem5blem2  42862  mapdindp0  42869  mapdindp2  42871  mapdindp4  42873  mapdh6lem2N  42884  mapdh6aN  42885  mapdh6dN  42889  mapdh6eN  42890  mapdh6hN  42893  hdmap1l6lem2  42958  hdmap1l6a  42959  hdmap1l6d  42963  hdmap1l6e  42964  hdmap1l6h  42967  hdmap11lem1  42991  hdmap11lem2  42992  hdmapneg  42996  hdmaprnlem3N  43000  hdmaprnlem3uN  43001  hdmaprnlem6N  43004  hdmaprnlem7N  43005  hdmaprnlem9N  43007  hdmaprnlem3eN  43008  hdmap14lem10  43027  hdmapinvlem3  43070  hdmapinvlem4  43071  hdmapglem7b  43078  hlhilphllem  43109  frlmsnic  43697  lincsumcl  49636