Theorem lspprid1

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

	Ref	Expression
Hypotheses	lspprid.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspprid.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspprid.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspprid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspprid.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	lspprid1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspprid.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspprid.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lspprid.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lspprid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5		lspprid.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6	4 5	prssd	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
7		snsspr1	⊢ { 𝑋 } ⊆ { 𝑋 , 𝑌 }
8	7	a1i	⊢ ( 𝜑 → { 𝑋 } ⊆ { 𝑋 , 𝑌 } )
9	1 2	lspss	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ∧ { 𝑋 } ⊆ { 𝑋 , 𝑌 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
10	3 6 8 9	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
11		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
12	1 11 2 3 4 5	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
13	1 11 2 3 12 4	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
14	10 13	mpbird	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )