This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ellspsn

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 ellspsn 
|- ( ( 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 ) ) )