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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmelpr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmelpr.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmelpr.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsmelpr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lsmelpr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lsmelpr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion lsmelpr ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmelpr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmelpr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lsmelpr.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsmelpr.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lsmelpr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lsmelpr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lsmelpr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 1 8 2 4 6 7 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
10 1 8 2 4 9 5 ellspsn5b ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) )
11 1 2 3 4 6 7 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) )
12 11 sseq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ) )
13 10 12 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ) )