Theorem lmodvacl 20872

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  Grpcgrp 18907  LModclmod 20857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910  df-lmod 20859

This theorem is referenced by:  lmodcom  20905  lmodvsghm  20920  lss1  20935  lspprabs  21092  lspabs2  21120  lspabs3  21121  lspfixed  21128  lspexch  21129  lspsolvlem  21142  ipdir  21621  ipdi  21622  ip2di  21623  ocvlss  21654  frlmphl  21763  frlmup1  21780  nmparlem  25231  minveclem2  25418  lsatfixedN  39508  lfl0f  39568  lfladdcl  39570  lflnegcl  39574  lflvscl  39576  lkrlss  39594  lshpkrlem5  39613  lshpkrlem6  39614  dvh3dim2  41947  dvh3dim3N  41948  lcfrlem17  42058  lcfrlem19  42060  lcfrlem20  42061  lcfrlem23  42064  baerlem3lem1  42206  baerlem5alem1  42207  baerlem5blem1  42208  baerlem5alem2  42210  baerlem5blem2  42211  mapdindp0  42218  mapdindp2  42220  mapdindp4  42222  mapdh6lem2N  42233  mapdh6aN  42234  mapdh6dN  42238  mapdh6eN  42239  mapdh6hN  42242  hdmap1l6lem2  42307  hdmap1l6a  42308  hdmap1l6d  42312  hdmap1l6e  42313  hdmap1l6h  42316  hdmap11lem1  42340  hdmap11lem2  42341  hdmapneg  42345  hdmaprnlem3N  42349  hdmaprnlem3uN  42350  hdmaprnlem6N  42353  hdmaprnlem7N  42354  hdmaprnlem9N  42356  hdmaprnlem3eN  42357  hdmap14lem10  42376  hdmapinvlem3  42419  hdmapinvlem4  42420  hdmapglem7b  42427  hlhilphllem  42458  frlmsnic  43033  lincsumcl  48929