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 ) ) ) ) ) )