![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-frlm | Structured version Visualization version GIF version |
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 21141 that an element of a direct sum has finitely many nonzero coordinates. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
df-frlm | β’ freeLMod = (π β V, π β V β¦ (π βm (π Γ {(ringLModβπ)}))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfrlm 21155 | . 2 class freeLMod | |
2 | vr | . . 3 setvar π | |
3 | vi | . . 3 setvar π | |
4 | cvv 3446 | . . 3 class V | |
5 | 2 | cv 1541 | . . . 4 class π |
6 | 3 | cv 1541 | . . . . 5 class π |
7 | crglmod 20633 | . . . . . . 7 class ringLMod | |
8 | 5, 7 | cfv 6497 | . . . . . 6 class (ringLModβπ) |
9 | 8 | csn 4587 | . . . . 5 class {(ringLModβπ)} |
10 | 6, 9 | cxp 5632 | . . . 4 class (π Γ {(ringLModβπ)}) |
11 | cdsmm 21140 | . . . 4 class βm | |
12 | 5, 10, 11 | co 7358 | . . 3 class (π βm (π Γ {(ringLModβπ)})) |
13 | 2, 3, 4, 4, 12 | cmpo 7360 | . 2 class (π β V, π β V β¦ (π βm (π Γ {(ringLModβπ)}))) |
14 | 1, 13 | wceq 1542 | 1 wff freeLMod = (π β V, π β V β¦ (π βm (π Γ {(ringLModβπ)}))) |
Colors of variables: wff setvar class |
This definition is referenced by: frlmval 21157 frlmrcl 21166 |
Copyright terms: Public domain | W3C validator |