Metamath Proof Explorer


Theorem lmodass

Description: Left module vector sum is associative. (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvacl.v V = Base W
lmodvacl.a + ˙ = + W
Assertion lmodass W LMod X V Y V Z V X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 lmodvacl.v V = Base W
2 lmodvacl.a + ˙ = + W
3 lmodgrp W LMod W Grp
4 1 2 grpass W Grp X V Y V Z V X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
5 3 4 sylan W LMod X V Y V Z V X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z