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	|- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrlm	|- freeLMod
1		vr	|- r
2		cvv	|- _V
3		vi	|- i
4	1	cv	|- r
5		cdsmm	|- (+)m
6	3	cv	|- i
7		crglmod	|- ringLMod
8	4 7	cfv	|- ( ringLMod ` r )
9	8	csn	|- { ( ringLMod ` r ) }
10	6 9	cxp	|- ( i X. { ( ringLMod ` r ) } )
11	4 10 5	co	|- ( r (+)m ( i X. { ( ringLMod ` r ) } ) )
12	1 3 2 2 11	cmpo	|- ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) )
13	0 12	wceq	|- freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) )