Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-frlm Structured version   Unicode version

Definition df-frlm 27172
Description: The  i-dimensional free module over a ring  r is the product of  i-many copies of the ring with componentwise addition and multiplication. If  i is infinite, the allowed vectors are restricted to those with finitely many nonzero coordinates; this ensures that the resulting module is actually spanned by its unit vectors. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Assertion
Ref Expression
df-frlm  |- freeLMod  =  ( r  e.  _V , 
i  e.  _V  |->  ( r  (+)m  ( i  X.  {
(ringLMod `  r ) } ) ) )
Distinct variable group:    i, r

Detailed syntax breakdown of Definition df-frlm
StepHypRef Expression
1 cfrlm 27170 . 2  class freeLMod
2 vr . . 3  set  r
3 vi . . 3  set  i
4 cvv 2948 . . 3  class  _V
52cv 1651 . . . 4  class  r
63cv 1651 . . . . 5  class  i
7 crglmod 16233 . . . . . . 7  class ringLMod
85, 7cfv 5446 . . . . . 6  class  (ringLMod `  r
)
98csn 3806 . . . . 5  class  { (ringLMod `  r ) }
106, 9cxp 4868 . . . 4  class  ( i  X.  { (ringLMod `  r
) } )
11 cdsmm 27155 . . . 4  class  (+)m
125, 10, 11co 6073 . . 3  class  ( r 
(+)m  ( i  X.  {
(ringLMod `  r ) } ) )
132, 3, 4, 4, 12cmpt2 6075 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  ( r 
(+)m  ( i  X.  {
(ringLMod `  r ) } ) ) )
141, 13wceq 1652 1  wff freeLMod  =  ( r  e.  _V , 
i  e.  _V  |->  ( r  (+)m  ( i  X.  {
(ringLMod `  r ) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  frlmval  27174  frlmrcl  27183
  Copyright terms: Public domain W3C validator