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	|- 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	lspprid1	|- ( ph -> X 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	4 5	prssd	|- ( ph -> { X , Y } C_ V )
7		snsspr1	|- { X } C_ { X , Y }
8	7	a1i	|- ( ph -> { X } C_ { X , Y } )
9	1 2	lspss	|- ( ( W e. LMod /\ { X , Y } C_ V /\ { X } C_ { X , Y } ) -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
10	3 6 8 9	syl3anc	|- ( ph -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
11		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
12	1 11 2 3 4 5	lspprcl	|- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
13	1 11 2 3 12 4	lspsnel5	|- ( ph -> ( X e. ( N ` { X , Y } ) <-> ( N ` { X } ) C_ ( N ` { X , Y } ) ) )
14	10 13	mpbird	|- ( ph -> X e. ( N ` { X , Y } ) )