Metamath Proof Explorer


Theorem lspprvacl

Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)

Ref Expression
Hypotheses lspprvacl.v V = Base W
lspprvacl.p + ˙ = + W
lspprvacl.n N = LSpan W
lspprvacl.w φ W LMod
lspprvacl.x φ X V
lspprvacl.y φ Y V
Assertion lspprvacl φ X + ˙ Y N X Y

Proof

Step Hyp Ref Expression
1 lspprvacl.v V = Base W
2 lspprvacl.p + ˙ = + W
3 lspprvacl.n N = LSpan W
4 lspprvacl.w φ W LMod
5 lspprvacl.x φ X V
6 lspprvacl.y φ Y V
7 eqid LSubSp W = LSubSp W
8 1 7 3 4 5 6 lspprcl φ N X Y LSubSp W
9 1 3 4 5 6 lspprid1 φ X N X Y
10 1 3 4 5 6 lspprid2 φ Y N X Y
11 2 7 lssvacl W LMod N X Y LSubSp W X N X Y Y N X Y X + ˙ Y N X Y
12 4 8 9 10 11 syl22anc φ X + ˙ Y N X Y