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
|- 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 ) } ) ) )