MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-frlm Structured version   Visualization version   GIF version

Definition df-frlm 21156
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.)
Assertion
Ref Expression
df-frlm freeLMod = (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ (π‘Ÿ βŠ•m (𝑖 Γ— {(ringLModβ€˜π‘Ÿ)})))
Distinct variable group:   𝑖,π‘Ÿ

Detailed syntax breakdown of Definition df-frlm
StepHypRef Expression
1 cfrlm 21155 . 2 class freeLMod
2 vr . . 3 setvar π‘Ÿ
3 vi . . 3 setvar 𝑖
4 cvv 3446 . . 3 class V
52cv 1541 . . . 4 class π‘Ÿ
63cv 1541 . . . . 5 class 𝑖
7 crglmod 20633 . . . . . . 7 class ringLMod
85, 7cfv 6497 . . . . . 6 class (ringLModβ€˜π‘Ÿ)
98csn 4587 . . . . 5 class {(ringLModβ€˜π‘Ÿ)}
106, 9cxp 5632 . . . 4 class (𝑖 Γ— {(ringLModβ€˜π‘Ÿ)})
11 cdsmm 21140 . . . 4 class βŠ•m
125, 10, 11co 7358 . . 3 class (π‘Ÿ βŠ•m (𝑖 Γ— {(ringLModβ€˜π‘Ÿ)}))
132, 3, 4, 4, 12cmpo 7360 . 2 class (π‘Ÿ ∈ V, 𝑖 ∈ V ↦ (π‘Ÿ βŠ•m (𝑖 Γ— {(ringLModβ€˜π‘Ÿ)})))
141, 13wceq 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