Theorem lspprel

Description: Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015)

	Ref	Expression
Hypotheses	lsppr.v	|- V = ( Base ` W )
	lsppr.a	|- .+ = ( +g ` W )
	lsppr.f	|- F = ( Scalar ` W )
	lsppr.k	|- K = ( Base ` F )
	lsppr.t	|- .x. = ( .s ` W )
	lsppr.n	|- N = ( LSpan ` W )
	lsppr.w	|- ( ph -> W e. LMod )
	lsppr.x	|- ( ph -> X e. V )
	lsppr.y	|- ( ph -> Y e. V )
Assertion	lspprel	|- ( ph -> ( Z e. ( N ` { X , Y } ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsppr.v	|- V = ( Base ` W )
2		lsppr.a	|- .+ = ( +g ` W )
3		lsppr.f	|- F = ( Scalar ` W )
4		lsppr.k	|- K = ( Base ` F )
5		lsppr.t	|- .x. = ( .s ` W )
6		lsppr.n	|- N = ( LSpan ` W )
7		lsppr.w	|- ( ph -> W e. LMod )
8		lsppr.x	|- ( ph -> X e. V )
9		lsppr.y	|- ( ph -> Y e. V )
10	1 2 3 4 5 6 7 8 9	lsppr	|- ( ph -> ( N ` { X , Y } ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )
11	10	eleq2d	|- ( ph -> ( Z e. ( N ` { X , Y } ) <-> Z e. { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } ) )
12		id	|- ( Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z = ( ( k .x. X ) .+ ( l .x. Y ) ) )
13		ovex	|- ( ( k .x. X ) .+ ( l .x. Y ) ) e. _V
14	12 13	eqeltrdi	|- ( Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
15	14	rexlimivw	|- ( E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
16	15	rexlimivw	|- ( E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
17		eqeq1	|- ( v = Z -> ( v = ( ( k .x. X ) .+ ( l .x. Y ) ) <-> Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
18	17	2rexbidv	|- ( v = Z -> ( E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
19	16 18	elab3	|- ( Z e. { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) )
20	11 19	bitrdi	|- ( ph -> ( Z e. ( N ` { X , Y } ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )