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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspprid.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspprid.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lspprid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspprid.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	lspprid2	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspprid.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspprid.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lspprid.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lspprid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5		lspprid.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
6	1 2 3 5 4	lspprid1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
7		prcom	⊢ { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
8	7	fveq2i	⊢ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } )
9	6 8	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )