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 20550 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 20564 | . 2 class freeLMod | |
2 | vr | . . 3 setvar 𝑟 | |
3 | vi | . . 3 setvar 𝑖 | |
4 | cvv 3398 | . . 3 class V | |
5 | 2 | cv 1541 | . . . 4 class 𝑟 |
6 | 3 | cv 1541 | . . . . 5 class 𝑖 |
7 | crglmod 20062 | . . . . . . 7 class ringLMod | |
8 | 5, 7 | cfv 6339 | . . . . . 6 class (ringLMod‘𝑟) |
9 | 8 | csn 4516 | . . . . 5 class {(ringLMod‘𝑟)} |
10 | 6, 9 | cxp 5523 | . . . 4 class (𝑖 × {(ringLMod‘𝑟)}) |
11 | cdsmm 20549 | . . . 4 class ⊕m | |
12 | 5, 10, 11 | co 7172 | . . 3 class (𝑟 ⊕m (𝑖 × {(ringLMod‘𝑟)})) |
13 | 2, 3, 4, 4, 12 | cmpo 7174 | . 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 20566 frlmrcl 20575 |
Copyright terms: Public domain | W3C validator |