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 | |
|
lbslsp.k | |
||
lbslsp.s | |
||
lbslsp.z | |
||
lbslsp.t | |
||
lbslsp.m | |
||
lbslsp.1 | |
||
Assertion | lbslsp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lbslsp.v | |
|
2 | lbslsp.k | |
|
3 | lbslsp.s | |
|
4 | lbslsp.z | |
|
5 | lbslsp.t | |
|
6 | lbslsp.m | |
|
7 | lbslsp.1 | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 1 8 9 | lbssp | |
11 | 7 10 | syl | |
12 | 11 | eleq2d | |
13 | 1 8 | lbsss | |
14 | 7 13 | syl | |
15 | 9 1 2 3 4 5 6 14 | ellspds | |
16 | 12 15 | bitr3d | |