# Metamath Proof Explorer

## Definition df-frlm

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 ${⊢}\mathrm{freeLMod}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼{r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrlm ${class}\mathrm{freeLMod}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vi ${setvar}{i}$
4 1 cv ${setvar}{r}$
5 cdsmm ${class}{\oplus }_{m}$
6 3 cv ${setvar}{i}$
7 crglmod ${class}\mathrm{ringLMod}$
8 4 7 cfv ${class}\mathrm{ringLMod}\left({r}\right)$
9 8 csn ${class}\left\{\mathrm{ringLMod}\left({r}\right)\right\}$
10 6 9 cxp ${class}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)$
11 4 10 5 co ${class}\left({r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)\right)$
12 1 3 2 2 11 cmpo ${class}\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼{r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)\right)$
13 0 12 wceq ${wff}\mathrm{freeLMod}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼{r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)\right)$