Theorem lmodvacl 20806

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  +_gcplusg 17158  Grpcgrp 18843  LModclmod 20791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-mgm 18545  df-sgrp 18624  df-mnd 18640  df-grp 18846  df-lmod 20793

This theorem is referenced by:  lmodcom  20839  lmodvsghm  20854  lss1  20869  lspprabs  21027  lspabs2  21055  lspabs3  21056  lspfixed  21063  lspexch  21064  lspsolvlem  21077  ipdir  21574  ipdi  21575  ip2di  21576  ocvlss  21607  frlmphl  21716  frlmup1  21733  nmparlem  25164  minveclem2  25351  lsatfixedN  39047  lfl0f  39107  lfladdcl  39109  lflnegcl  39113  lflvscl  39115  lkrlss  39133  lshpkrlem5  39152  lshpkrlem6  39153  dvh3dim2  41486  dvh3dim3N  41487  lcfrlem17  41597  lcfrlem19  41599  lcfrlem20  41600  lcfrlem23  41603  baerlem3lem1  41745  baerlem5alem1  41746  baerlem5blem1  41747  baerlem5alem2  41749  baerlem5blem2  41750  mapdindp0  41757  mapdindp2  41759  mapdindp4  41761  mapdh6lem2N  41772  mapdh6aN  41773  mapdh6dN  41777  mapdh6eN  41778  mapdh6hN  41781  hdmap1l6lem2  41846  hdmap1l6a  41847  hdmap1l6d  41851  hdmap1l6e  41852  hdmap1l6h  41855  hdmap11lem1  41879  hdmap11lem2  41880  hdmapneg  41884  hdmaprnlem3N  41888  hdmaprnlem3uN  41889  hdmaprnlem6N  41892  hdmaprnlem7N  41893  hdmaprnlem9N  41895  hdmaprnlem3eN  41896  hdmap14lem10  41915  hdmapinvlem3  41958  hdmapinvlem4  41959  hdmapglem7b  41966  hlhilphllem  41997  frlmsnic  42572  lincsumcl  48462