Theorem lmodvacl 20788

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Grpcgrp 18872  LModclmod 20773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875  df-lmod 20775

This theorem is referenced by:  lmodcom  20821  lmodvsghm  20836  lss1  20851  lspprabs  21009  lspabs2  21037  lspabs3  21038  lspfixed  21045  lspexch  21046  lspsolvlem  21059  ipdir  21555  ipdi  21556  ip2di  21557  ocvlss  21588  frlmphl  21697  frlmup1  21714  nmparlem  25146  minveclem2  25333  lsatfixedN  39009  lfl0f  39069  lfladdcl  39071  lflnegcl  39075  lflvscl  39077  lkrlss  39095  lshpkrlem5  39114  lshpkrlem6  39115  dvh3dim2  41449  dvh3dim3N  41450  lcfrlem17  41560  lcfrlem19  41562  lcfrlem20  41563  lcfrlem23  41566  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  baerlem5alem2  41712  baerlem5blem2  41713  mapdindp0  41720  mapdindp2  41722  mapdindp4  41724  mapdh6lem2N  41735  mapdh6aN  41736  mapdh6dN  41740  mapdh6eN  41741  mapdh6hN  41744  hdmap1l6lem2  41809  hdmap1l6a  41810  hdmap1l6d  41814  hdmap1l6e  41815  hdmap1l6h  41818  hdmap11lem1  41842  hdmap11lem2  41843  hdmapneg  41847  hdmaprnlem3N  41851  hdmaprnlem3uN  41852  hdmaprnlem6N  41855  hdmaprnlem7N  41856  hdmaprnlem9N  41858  hdmaprnlem3eN  41859  hdmap14lem10  41878  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem7b  41929  hlhilphllem  41960  frlmsnic  42535  lincsumcl  48424