Metamath Proof Explorer


Theorem lspprid2

Description: A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015)

Ref Expression
Hypotheses lspprid.v V = Base W
lspprid.n N = LSpan W
lspprid.w φ W LMod
lspprid.x φ X V
lspprid.y φ Y V
Assertion lspprid2 φ Y N X Y

Proof

Step Hyp Ref Expression
1 lspprid.v V = Base W
2 lspprid.n N = LSpan W
3 lspprid.w φ W LMod
4 lspprid.x φ X V
5 lspprid.y φ Y V
6 1 2 3 5 4 lspprid1 φ Y N Y X
7 prcom Y X = X Y
8 7 fveq2i N Y X = N X Y
9 6 8 eleqtrdi φ Y N X Y