Metamath Proof Explorer


Theorem lsmelpr

Description: Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses lsmelpr.v V = Base W
lsmelpr.n N = LSpan W
lsmelpr.p ˙ = LSSum W
lsmelpr.w φ W LMod
lsmelpr.x φ X V
lsmelpr.y φ Y V
lsmelpr.z φ Z V
Assertion lsmelpr φ X N Y Z N X N Y ˙ N Z

Proof

Step Hyp Ref Expression
1 lsmelpr.v V = Base W
2 lsmelpr.n N = LSpan W
3 lsmelpr.p ˙ = LSSum W
4 lsmelpr.w φ W LMod
5 lsmelpr.x φ X V
6 lsmelpr.y φ Y V
7 lsmelpr.z φ Z V
8 eqid LSubSp W = LSubSp W
9 1 8 2 4 6 7 lspprcl φ N Y Z LSubSp W
10 1 8 2 4 9 5 lspsnel5 φ X N Y Z N X N Y Z
11 1 2 3 4 6 7 lsmpr φ N Y Z = N Y ˙ N Z
12 11 sseq2d φ N X N Y Z N X N Y ˙ N Z
13 10 12 bitrd φ X N Y Z N X N Y ˙ N Z