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

Metamath Proof Explorer

Theorem lbslsp

Description: Any element of a left module M can be expressed as a linear combination of the elements of a basis V of M . (Contributed by Thierry Arnoux, 3-Aug-2023)

Ref Expression
Hypotheses lbslsp.v 
|- B = ( Base ` M )
lbslsp.k 
|- K = ( Base ` S )
lbslsp.s 
|- S = ( Scalar ` M )
lbslsp.z 
|- .0. = ( 0g ` S )
lbslsp.t 
|- .x. = ( .s ` M )
lbslsp.m 
|- ( ph -> M e. LMod )
lbslsp.1 
|- ( ph -> V e. ( LBasis ` M ) )
Assertion lbslsp 
|- ( ph -> ( X e. B <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lbslsp.v 
 |-  B = ( Base ` M )
2 lbslsp.k 
 |-  K = ( Base ` S )
3 lbslsp.s 
 |-  S = ( Scalar ` M )
4 lbslsp.z 
 |-  .0. = ( 0g ` S )
5 lbslsp.t 
 |-  .x. = ( .s ` M )
6 lbslsp.m 
 |-  ( ph -> M e. LMod )
7 lbslsp.1 
 |-  ( ph -> V e. ( LBasis ` M ) )
8 eqid 
 |-  ( LBasis ` M ) = ( LBasis ` M )
9 eqid 
 |-  ( LSpan ` M ) = ( LSpan ` M )
10 1 8 9 lbssp 
 |-  ( V e. ( LBasis ` M ) -> ( ( LSpan ` M ) ` V ) = B )
11 7 10 syl 
 |-  ( ph -> ( ( LSpan ` M ) ` V ) = B )
12 11 eleq2d 
 |-  ( ph -> ( X e. ( ( LSpan ` M ) ` V ) <-> X e. B ) )
13 1 8 lbsss 
 |-  ( V e. ( LBasis ` M ) -> V C_ B )
14 7 13 syl 
 |-  ( ph -> V C_ B )
15 9 1 2 3 4 5 6 14 ellspds 
 |-  ( ph -> ( X e. ( ( LSpan ` M ) ` V ) <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )
16 12 15 bitr3d 
 |-  ( ph -> ( X e. B <-> E. a e. ( K ^m V ) ( a finSupp .0. /\ X = ( M gsum ( v e. V |-> ( ( a ` v ) .x. v ) ) ) ) ) )