Metamath Proof Explorer


Theorem lmodvacl

Description: Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvacl.v V=BaseW
lmodvacl.a +˙=+W
Assertion lmodvacl WLModXVYVX+˙YV

Proof

Step Hyp Ref Expression
1 lmodvacl.v V=BaseW
2 lmodvacl.a +˙=+W
3 lmodgrp WLModWGrp
4 1 2 grpcl WGrpXVYVX+˙YV
5 3 4 syl3an1 WLModXVYVX+˙YV