Description: Define the function associating with a ring and a set the direct sum indexed by that set of copies of that ring regarded as a left module over itself. Recall from df-dsmm that an element of a direct sum has finitely many nonzero coordinates. (Contributed by Stefan O'Rear, 1-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-frlm | |- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfrlm | |- freeLMod |
|
1 | vr | |- r |
|
2 | cvv | |- _V |
|
3 | vi | |- i |
|
4 | 1 | cv | |- r |
5 | cdsmm | |- (+)m |
|
6 | 3 | cv | |- i |
7 | crglmod | |- ringLMod |
|
8 | 4 7 | cfv | |- ( ringLMod ` r ) |
9 | 8 | csn | |- { ( ringLMod ` r ) } |
10 | 6 9 | cxp | |- ( i X. { ( ringLMod ` r ) } ) |
11 | 4 10 5 | co | |- ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) |
12 | 1 3 2 2 11 | cmpo | |- ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) ) |
13 | 0 12 | wceq | |- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) ) |