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\times \left\{\mathrm{ringLMod}\left(r\right)\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrlm	$$class\mathrm{freeLMod}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4	1	cv	$$setvarr$$
5		cdsmm	$$class{\oplus }_m$$
6	3	cv	$$setvari$$
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\times \left\{\mathrm{ringLMod}\left(r\right)\right\}\right)$$
11	4 10 5	co	$$class\left(r{\oplus }_m\left(i\times \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\times \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\times \left\{\mathrm{ringLMod}\left(r\right)\right\}\right)\right)$$