Theorem lmodvacl 20781

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  Grpcgrp 18865  LModclmod 20766

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 2701  ax-nul 5261

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-grp 18868  df-lmod 20768

This theorem is referenced by:  lmodcom  20814  lmodvsghm  20829  lss1  20844  lspprabs  21002  lspabs2  21030  lspabs3  21031  lspfixed  21038  lspexch  21039  lspsolvlem  21052  ipdir  21548  ipdi  21549  ip2di  21550  ocvlss  21581  frlmphl  21690  frlmup1  21707  nmparlem  25139  minveclem2  25326  lsatfixedN  39002  lfl0f  39062  lfladdcl  39064  lflnegcl  39068  lflvscl  39070  lkrlss  39088  lshpkrlem5  39107  lshpkrlem6  39108  dvh3dim2  41442  dvh3dim3N  41443  lcfrlem17  41553  lcfrlem19  41555  lcfrlem20  41556  lcfrlem23  41559  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  baerlem5alem2  41705  baerlem5blem2  41706  mapdindp0  41713  mapdindp2  41715  mapdindp4  41717  mapdh6lem2N  41728  mapdh6aN  41729  mapdh6dN  41733  mapdh6eN  41734  mapdh6hN  41737  hdmap1l6lem2  41802  hdmap1l6a  41803  hdmap1l6d  41807  hdmap1l6e  41808  hdmap1l6h  41811  hdmap11lem1  41835  hdmap11lem2  41836  hdmapneg  41840  hdmaprnlem3N  41844  hdmaprnlem3uN  41845  hdmaprnlem6N  41848  hdmaprnlem7N  41849  hdmaprnlem9N  41851  hdmaprnlem3eN  41852  hdmap14lem10  41871  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem7b  41922  hlhilphllem  41953  frlmsnic  42528  lincsumcl  48420