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

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 ellspsn5b ⊢ φ → 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