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=BaseM
lbslsp.k K=BaseS
lbslsp.s S=ScalarM
lbslsp.z 0˙=0S
lbslsp.t ·˙=M
lbslsp.m φMLMod
lbslsp.1 φVLBasisM
Assertion lbslsp φXBaKVfinSupp0˙aX=MvVav·˙v

Proof

Step Hyp Ref Expression
1 lbslsp.v B=BaseM
2 lbslsp.k K=BaseS
3 lbslsp.s S=ScalarM
4 lbslsp.z 0˙=0S
5 lbslsp.t ·˙=M
6 lbslsp.m φMLMod
7 lbslsp.1 φVLBasisM
8 eqid LBasisM=LBasisM
9 eqid LSpanM=LSpanM
10 1 8 9 lbssp VLBasisMLSpanMV=B
11 7 10 syl φLSpanMV=B
12 11 eleq2d φXLSpanMVXB
13 1 8 lbsss VLBasisMVB
14 7 13 syl φVB
15 9 1 2 3 4 5 6 14 ellspds φXLSpanMVaKVfinSupp0˙aX=MvVav·˙v
16 12 15 bitr3d φXBaKVfinSupp0˙aX=MvVav·˙v