Theorem lspprss

Description: The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015)

	Ref	Expression
Hypotheses	lspprss.s	|- S = ( LSubSp ` W )
	lspprss.n	|- N = ( LSpan ` W )
	lspprss.w	|- ( ph -> W e. LMod )
	lspprss.u	|- ( ph -> U e. S )
	lspprss.x	|- ( ph -> X e. U )
	lspprss.y	|- ( ph -> Y e. U )
Assertion	lspprss	|- ( ph -> ( N ` { X , Y } ) C_ U )

Proof

Step	Hyp	Ref	Expression
1		lspprss.s	|- S = ( LSubSp ` W )
2		lspprss.n	|- N = ( LSpan ` W )
3		lspprss.w	|- ( ph -> W e. LMod )
4		lspprss.u	|- ( ph -> U e. S )
5		lspprss.x	|- ( ph -> X e. U )
6		lspprss.y	|- ( ph -> Y e. U )
7	5 6	prssd	|- ( ph -> { X , Y } C_ U )
8	1 2	lspssp	|- ( ( W e. LMod /\ U e. S /\ { X , Y } C_ U ) -> ( N ` { X , Y } ) C_ U )
9	3 4 7 8	syl3anc	|- ( ph -> ( N ` { X , Y } ) C_ U )