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

Metamath Proof Explorer

Theorem lspfval

Description: The span function for a left vector space (or a left module). ( df-span analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspval.v 
|- V = ( Base ` W )
lspval.s 
|- S = ( LSubSp ` W )
lspval.n 
|- N = ( LSpan ` W )
Assertion lspfval 
|- ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )

Proof

Step Hyp Ref Expression
1 lspval.v 
 |-  V = ( Base ` W )
2 lspval.s 
 |-  S = ( LSubSp ` W )
3 lspval.n 
 |-  N = ( LSpan ` W )
4 elex 
 |-  ( W e. X -> W e. _V )
5 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
6 5 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
7 6 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P V )
8 fveq2 
 |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
9 8 2 eqtr4di 
 |-  ( w = W -> ( LSubSp ` w ) = S )
10 9 rabeqdv 
 |-  ( w = W -> { t e. ( LSubSp ` w ) | s C_ t } = { t e. S | s C_ t } )
11 10 inteqd 
 |-  ( w = W -> |^| { t e. ( LSubSp ` w ) | s C_ t } = |^| { t e. S | s C_ t } )
12 7 11 mpteq12dv 
 |-  ( w = W -> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
13 df-lsp 
 |-  LSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. ( LSubSp ` w ) | s C_ t } ) )
14 1 fvexi 
 |-  V e. _V
15 14 pwex 
 |-  ~P V e. _V
16 15 mptex 
 |-  ( s e. ~P V |-> |^| { t e. S | s C_ t } ) e. _V
17 12 13 16 fvmpt 
 |-  ( W e. _V -> ( LSpan ` W ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
18 4 17 syl 
 |-  ( W e. X -> ( LSpan ` W ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
19 3 18 eqtrid 
 |-  ( W e. X -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )