Theorem lsmelpr

Description: Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015)

	Ref	Expression
Hypotheses	lsmelpr.v	|- V = ( Base ` W )
	lsmelpr.n	|- N = ( LSpan ` W )
	lsmelpr.p	|- .(+) = ( LSSum ` W )
	lsmelpr.w	|- ( ph -> W e. LMod )
	lsmelpr.x	|- ( ph -> X e. V )
	lsmelpr.y	|- ( ph -> Y e. V )
	lsmelpr.z	|- ( ph -> Z e. V )
Assertion	lsmelpr	|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmelpr.v	|- V = ( Base ` W )
2		lsmelpr.n	|- N = ( LSpan ` W )
3		lsmelpr.p	|- .(+) = ( LSSum ` W )
4		lsmelpr.w	|- ( ph -> W e. LMod )
5		lsmelpr.x	|- ( ph -> X e. V )
6		lsmelpr.y	|- ( ph -> Y e. V )
7		lsmelpr.z	|- ( ph -> Z e. V )
8		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
9	1 8 2 4 6 7	lspprcl	|- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
10	1 8 2 4 9 5	ellspsn5b	|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
11	1 2 3 4 6 7	lsmpr	|- ( ph -> ( N ` { Y , Z } ) = ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) )
12	11	sseq2d	|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )
13	10 12	bitrd	|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )