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	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ) )