Theorem lspsnel

Description: Member of span of the singleton of a vector. ( elspansn analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspsn.f	|- F = ( Scalar ` W )
	lspsn.k	|- K = ( Base ` F )
	lspsn.v	|- V = ( Base ` W )
	lspsn.t	|- .x. = ( .s ` W )
	lspsn.n	|- N = ( LSpan ` W )
Assertion	lspsnel	|- ( ( W e. LMod /\ X e. V ) -> ( U e. ( N ` { X } ) <-> E. k e. K U = ( k .x. X ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspsn.f	|- F = ( Scalar ` W )
2		lspsn.k	|- K = ( Base ` F )
3		lspsn.v	|- V = ( Base ` W )
4		lspsn.t	|- .x. = ( .s ` W )
5		lspsn.n	|- N = ( LSpan ` W )
6	1 2 3 4 5	lspsn	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) = { v | E. k e. K v = ( k .x. X ) } )
7	6	eleq2d	|- ( ( W e. LMod /\ X e. V ) -> ( U e. ( N ` { X } ) <-> U e. { v | E. k e. K v = ( k .x. X ) } ) )
8		id	|- ( U = ( k .x. X ) -> U = ( k .x. X ) )
9		ovex	|- ( k .x. X ) e. _V
10	8 9	eqeltrdi	|- ( U = ( k .x. X ) -> U e. _V )
11	10	rexlimivw	|- ( E. k e. K U = ( k .x. X ) -> U e. _V )
12		eqeq1	|- ( v = U -> ( v = ( k .x. X ) <-> U = ( k .x. X ) ) )
13	12	rexbidv	|- ( v = U -> ( E. k e. K v = ( k .x. X ) <-> E. k e. K U = ( k .x. X ) ) )
14	11 13	elab3	|- ( U e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K U = ( k .x. X ) )
15	7 14	bitrdi	|- ( ( W e. LMod /\ X e. V ) -> ( U e. ( N ` { X } ) <-> E. k e. K U = ( k .x. X ) ) )