Metamath Proof Explorer

Theorem lspsn

Description: Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014) (Proof shortened 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 lspsn 
|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) = { v | E. k e. K v = ( 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 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
7 simpl 
 |-  ( ( W e. LMod /\ X e. V ) -> W e. LMod )
8 3 1 4 2 6 lss1d 
 |-  ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } e. ( LSubSp ` W ) )
9 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
10 1 2 9 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` F ) e. K )
11 3 1 4 9 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
12 11 eqcomd 
 |-  ( ( W e. LMod /\ X e. V ) -> X = ( ( 1r ` F ) .x. X ) )
13 oveq1 
 |-  ( k = ( 1r ` F ) -> ( k .x. X ) = ( ( 1r ` F ) .x. X ) )
14 13 rspceeqv 
 |-  ( ( ( 1r ` F ) e. K /\ X = ( ( 1r ` F ) .x. X ) ) -> E. k e. K X = ( k .x. X ) )
15 10 12 14 syl2an2r 
 |-  ( ( W e. LMod /\ X e. V ) -> E. k e. K X = ( k .x. X ) )
16 eqeq1 
 |-  ( v = X -> ( v = ( k .x. X ) <-> X = ( k .x. X ) ) )
17 16 rexbidv 
 |-  ( v = X -> ( E. k e. K v = ( k .x. X ) <-> E. k e. K X = ( k .x. X ) ) )
18 17 elabg 
 |-  ( X e. V -> ( X e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K X = ( k .x. X ) ) )
19 18 adantl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( X e. { v | E. k e. K v = ( k .x. X ) } <-> E. k e. K X = ( k .x. X ) ) )
20 15 19 mpbird 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. { v | E. k e. K v = ( k .x. X ) } )
21 6 5 7 8 20 lspsnel5a 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) C_ { v | E. k e. K v = ( k .x. X ) } )
22 7 adantr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> W e. LMod )
23 3 6 5 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
24 23 adantr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
25 simpr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> k e. K )
26 3 5 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
27 26 adantr 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> X e. ( N ` { X } ) )
28 1 4 2 6 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) ) /\ ( k e. K /\ X e. ( N ` { X } ) ) ) -> ( k .x. X ) e. ( N ` { X } ) )
29 22 24 25 27 28 syl22anc 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> ( k .x. X ) e. ( N ` { X } ) )
30 eleq1a 
 |-  ( ( k .x. X ) e. ( N ` { X } ) -> ( v = ( k .x. X ) -> v e. ( N ` { X } ) ) )
31 29 30 syl 
 |-  ( ( ( W e. LMod /\ X e. V ) /\ k e. K ) -> ( v = ( k .x. X ) -> v e. ( N ` { X } ) ) )
32 31 rexlimdva 
 |-  ( ( W e. LMod /\ X e. V ) -> ( E. k e. K v = ( k .x. X ) -> v e. ( N ` { X } ) ) )
33 32 abssdv 
 |-  ( ( W e. LMod /\ X e. V ) -> { v | E. k e. K v = ( k .x. X ) } C_ ( N ` { X } ) )
34 21 33 eqssd 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) = { v | E. k e. K v = ( k .x. X ) } )