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

Metamath Proof Explorer

Theorem elfilspd

Description: Simplified version of ellspd when the spanning set is finite: all linear combinations are then acceptable. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

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 )
elfilspd.f 
|- ( ph -> F : I --> B )
elfilspd.m 
|- ( ph -> M e. LMod )
elfilspd.i 
|- ( ph -> I e. Fin )
Assertion elfilspd 
|- ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) 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 elfilspd.f 
 |-  ( ph -> F : I --> B )
8 elfilspd.m 
 |-  ( ph -> M e. LMod )
9 elfilspd.i 
 |-  ( ph -> I e. Fin )
10 1 2 3 4 5 6 7 8 9 ellspd 
 |-  ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
11 elmapi 
 |-  ( f e. ( K ^m I ) -> f : I --> K )
12 11 adantl 
 |-  ( ( ph /\ f e. ( K ^m I ) ) -> f : I --> K )
13 9 adantr 
 |-  ( ( ph /\ f e. ( K ^m I ) ) -> I e. Fin )
14 5 fvexi 
 |-  .0. e. _V
15 14 a1i 
 |-  ( ( ph /\ f e. ( K ^m I ) ) -> .0. e. _V )
16 12 13 15 fdmfifsupp 
 |-  ( ( ph /\ f e. ( K ^m I ) ) -> f finSupp .0. )
17 16 biantrurd 
 |-  ( ( ph /\ f e. ( K ^m I ) ) -> ( X = ( M gsum ( f oF .x. F ) ) <-> ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
18 17 rexbidva 
 |-  ( ph -> ( E. f e. ( K ^m I ) X = ( M gsum ( f oF .x. F ) ) <-> E. f e. ( K ^m I ) ( f finSupp .0. /\ X = ( M gsum ( f oF .x. F ) ) ) ) )
19 10 18 bitr4d 
 |-  ( ph -> ( X e. ( N ` ( F " I ) ) <-> E. f e. ( K ^m I ) X = ( M gsum ( f oF .x. F ) ) ) )