Theorem lmodvacl 19100

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

Syntax hints:   → wi 4   ∧ w3a 1072   = wceq 1632   ∈ wcel 2140  ‘cfv 6050  (class class class)co 6815  Basecbs 16080  +_gcplusg 16164  Grpcgrp 17644  LModclmod 19086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-nul 4942

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-mgm 17464  df-sgrp 17506  df-mnd 17517  df-grp 17647  df-lmod 19088

This theorem is referenced by:  lmodcom  19132  lmodvsghm  19147  lss1  19162  lspprabs  19318  lspabs2  19343  lspabs3  19344  lspfixed  19351  lspexch  19352  lspsolvlem  19365  ipdir  20207  ipdi  20208  ip2di  20209  ocvlss  20239  frlmphl  20343  frlmup1  20360  nmparlem  23259  minveclem2  23418  lsatfixedN  34818  lfl0f  34878  lfladdcl  34880  lflnegcl  34884  lflvscl  34886  lkrlss  34904  lshpkrlem5  34923  lshpkrlem6  34924  dvh3dim2  37258  dvh3dim3N  37259  lcfrlem17  37369  lcfrlem19  37371  lcfrlem20  37372  lcfrlem23  37375  baerlem3lem1  37517  baerlem5alem1  37518  baerlem5blem1  37519  baerlem5alem2  37521  baerlem5blem2  37522  mapdindp0  37529  mapdindp2  37531  mapdindp4  37533  mapdh6lem2N  37544  mapdh6aN  37545  mapdh6dN  37549  mapdh6eN  37550  mapdh6hN  37553  hdmap1l6lem2  37619  hdmap1l6a  37620  hdmap1l6d  37624  hdmap1l6e  37625  hdmap1l6h  37628  hdmap11lem1  37654  hdmap11lem2  37655  hdmapneg  37659  hdmaprnlem3N  37663  hdmaprnlem3uN  37664  hdmaprnlem6N  37667  hdmaprnlem7N  37668  hdmaprnlem9N  37670  hdmaprnlem3eN  37671  hdmap14lem10  37690  hdmapinvlem3  37733  hdmapinvlem4  37734  hdmapglem7b  37741  hlhilphllem  37772  lincsumcl  42749