Metamath Proof Explorer

Theorem ellspd

Description: The elements of the span of an indexed collection of basic vectors are those vectors which can be written as finite linear combinations of basic vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by AV, 24-Jun-2019) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses ellspd.n 
|- N = ( LSpan ` M )
ellspd.v 
|- B = ( Base ` M )
ellspd.k 
|- K = ( Base ` S )
ellspd.s 
|- S = ( Scalar ` M )
ellspd.z 
|- .0. = ( 0g ` S )
ellspd.t 
|- .x. = ( .s ` M )
ellspd.f 
|- ( ph -> F : I --> B )
ellspd.m 
|- ( ph -> M e. LMod )
ellspd.i 
|- ( ph -> I e. V )
Assertion ellspd 
|- ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ellspd.n 
 |-  N = ( LSpan ` M )
2 ellspd.v 
 |-  B = ( Base ` M )
3 ellspd.k 
 |-  K = ( Base ` S )
4 ellspd.s 
 |-  S = ( Scalar ` M )
5 ellspd.z 
 |-  .0. = ( 0g ` S )
6 ellspd.t 
 |-  .x. = ( .s ` M )
7 ellspd.f 
 |-  ( ph -> F : I --> B )
8 ellspd.m 
 |-  ( ph -> M e. LMod )
9 ellspd.i 
 |-  ( ph -> I e. V )
10 ffn 
 |-  ( F : I --> B -> F Fn I )
11 fnima 
 |-  ( F Fn I -> ( F " I ) = ran F )
12 7 10 11 3syl 
 |-  ( ph -> ( F " I ) = ran F )
13 12 fveq2d 
 |-  ( ph -> ( N ` ( F " I ) ) = ( N ` ran F ) )
14 eqid 
 |-  ( f e. ( Base ` ( S freeLMod I ) ) |-> ( M gsum ( f oF .x. F ) ) ) = ( f e. ( Base ` ( S freeLMod I ) ) |-> ( M gsum ( f oF .x. F ) ) )
15 14 rnmpt 
 |-  ran ( f e. ( Base ` ( S freeLMod I ) ) |-> ( M gsum ( f oF .x. F ) ) ) = { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) }
16 eqid 
 |-  ( S freeLMod I ) = ( S freeLMod I )
17 eqid 
 |-  ( Base ` ( S freeLMod I ) ) = ( Base ` ( S freeLMod I ) )
18 4 a1i 
 |-  ( ph -> S = ( Scalar ` M ) )
19 16 17 2 6 14 8 9 18 7 1 frlmup3 
 |-  ( ph -> ran ( f e. ( Base ` ( S freeLMod I ) ) |-> ( M gsum ( f oF .x. F ) ) ) = ( N ` ran F ) )
20 15 19 syl5eqr 
 |-  ( ph -> { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) } = ( N ` ran F ) )
21 13 20 eqtr4d 
 |-  ( ph -> ( N ` ( F " I ) ) = { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) } )
22 21 eleq2d 
 |-  ( ph -> ( X e. ( N ` ( F " I ) ) <-> X e. { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) } ) )
23 ovex 
 |-  ( M gsum ( f oF .x. F ) ) e. _V
24 eleq1 
 |-  ( X = ( M gsum ( f oF .x. F ) ) -> ( X e. _V <-> ( M gsum ( f oF .x. F ) ) e. _V ) )
25 23 24 mpbiri 
 |-  ( X = ( M gsum ( f oF .x. F ) ) -> X e. _V )
26 25 rexlimivw 
 |-  ( E. f e. ( Base ` ( S freeLMod I ) ) X = ( M gsum ( f oF .x. F ) ) -> X e. _V )
27 eqeq1 
 |-  ( a = X -> ( a = ( M gsum ( f oF .x. F ) ) <-> X = ( M gsum ( f oF .x. F ) ) ) )
28 27 rexbidv 
 |-  ( a = X -> ( E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) <-> E. f e. ( Base ` ( S freeLMod I ) ) X = ( M gsum ( f oF .x. F ) ) ) )
29 26 28 elab3 
 |-  ( X e. { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) } <-> E. f e. ( Base ` ( S freeLMod I ) ) X = ( M gsum ( f oF .x. F ) ) )
30 4 fvexi 
 |-  S e. _V
31 eqid 
 |-  { a e. ( K ^m I ) | a finSupp .0. } = { a e. ( K ^m I ) | a finSupp .0. }
32 16 3 5 31 frlmbas 
 |-  ( ( S e. _V /\ I e. V ) -> { a e. ( K ^m I ) | a finSupp .0. } = ( Base ` ( S freeLMod I ) ) )
33 30 9 32 sylancr 
 |-  ( ph -> { a e. ( K ^m I ) | a finSupp .0. } = ( Base ` ( S freeLMod I ) ) )
34 33 eqcomd 
 |-  ( ph -> ( Base ` ( S freeLMod I ) ) = { a e. ( K ^m I ) | a finSupp .0. } )
35 34 rexeqdv 
 |-  ( ph -> ( E. f e. ( Base ` ( S freeLMod I ) ) X = ( M gsum ( f oF .x. F ) ) <-> E. f e. { a e. ( K ^m I ) | a finSupp .0. } X = ( M gsum ( f oF .x. F ) ) ) )
36 breq1 
 |-  ( a = f -> ( a finSupp .0. <-> f finSupp .0. ) )
37 36 rexrab 
 |-  ( E. f e. { a e. ( K ^m I ) | a finSupp .0. } X = ( M gsum ( f oF .x. F ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) )
38 35 37 bitrdi 
 |-  ( ph -> ( E. f e. ( Base ` ( S freeLMod I ) ) X = ( M gsum ( f oF .x. F ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
39 29 38 syl5bb 
 |-  ( ph -> ( X e. { a | E. f e. ( Base ` ( S freeLMod I ) ) a = ( M gsum ( f oF .x. F ) ) } <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
40 22 39 bitrd 
 |-  ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )