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	|- V = ( Base ` W )
	lspprid.n	|- N = ( LSpan ` W )
	lspprid.w	|- ( ph -> W e. LMod )
	lspprid.x	|- ( ph -> X e. V )
	lspprid.y	|- ( ph -> Y e. V )
Assertion	lspprid2	|- ( ph -> Y e. ( N ` { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lspprid.v	|- V = ( Base ` W )
2		lspprid.n	|- N = ( LSpan ` W )
3		lspprid.w	|- ( ph -> W e. LMod )
4		lspprid.x	|- ( ph -> X e. V )
5		lspprid.y	|- ( ph -> Y e. V )
6	1 2 3 5 4	lspprid1	|- ( ph -> Y e. ( N ` { Y , X } ) )
7		prcom	|- { Y , X } = { X , Y }
8	7	fveq2i	|- ( N ` { Y , X } ) = ( N ` { X , Y } )
9	6 8	eleqtrdi	|- ( ph -> Y e. ( N ` { X , Y } ) )