This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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