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

Metamath Proof Explorer

Theorem lspval

Description: The span of a set of vectors (in a left module). ( spanval 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 lspval 
|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U 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 1 2 3 lspfval 
 |-  ( W e. LMod -> N = ( s e. ~P V |-> |^| { t e. S | s C_ t } ) )
5 4 fveq1d 
 |-  ( W e. LMod -> ( N ` U ) = ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) )
6 5 adantr 
 |-  ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) )
7 eqid 
 |-  ( s e. ~P V |-> |^| { t e. S | s C_ t } ) = ( s e. ~P V |-> |^| { t e. S | s C_ t } )
8 sseq1 
 |-  ( s = U -> ( s C_ t <-> U C_ t ) )
9 8 rabbidv 
 |-  ( s = U -> { t e. S | s C_ t } = { t e. S | U C_ t } )
10 9 inteqd 
 |-  ( s = U -> |^| { t e. S | s C_ t } = |^| { t e. S | U C_ t } )
11 simpr 
 |-  ( ( W e. LMod /\ U C_ V ) -> U C_ V )
12 1 fvexi 
 |-  V e. _V
13 12 elpw2 
 |-  ( U e. ~P V <-> U C_ V )
14 11 13 sylibr 
 |-  ( ( W e. LMod /\ U C_ V ) -> U e. ~P V )
15 1 2 lss1 
 |-  ( W e. LMod -> V e. S )
16 sseq2 
 |-  ( t = V -> ( U C_ t <-> U C_ V ) )
17 16 rspcev 
 |-  ( ( V e. S /\ U C_ V ) -> E. t e. S U C_ t )
18 15 17 sylan 
 |-  ( ( W e. LMod /\ U C_ V ) -> E. t e. S U C_ t )
19 intexrab 
 |-  ( E. t e. S U C_ t <-> |^| { t e. S | U C_ t } e. _V )
20 18 19 sylib 
 |-  ( ( W e. LMod /\ U C_ V ) -> |^| { t e. S | U C_ t } e. _V )
21 7 10 14 20 fvmptd3 
 |-  ( ( W e. LMod /\ U C_ V ) -> ( ( s e. ~P V |-> |^| { t e. S | s C_ t } ) ` U ) = |^| { t e. S | U C_ t } )
22 6 21 eqtrd 
 |-  ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. S | U C_ t } )