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

Definition df-frlm 27317
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 27315 . 2  class freeLMod
2 vr . . 3  set  r
3 vi . . 3  set  i
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . 4  class  r
63cv 1631 . . . . 5  class  i
7 crglmod 15938 . . . . . . 7  class ringLMod
85, 7cfv 5271 . . . . . 6  class  (ringLMod `  r
)
98csn 3653 . . . . 5  class  { (ringLMod `  r ) }
106, 9cxp 4703 . . . 4  class  ( i  X.  { (ringLMod `  r
) } )
11 cdsmm 27300 . . . 4  class  (+)m
125, 10, 11co 5874 . . 3  class  ( r 
(+)m  ( i  X.  {
(ringLMod `  r ) } ) )
132, 3, 4, 4, 12cmpt2 5876 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  ( r 
(+)m  ( i  X.  {
(ringLMod `  r ) } ) ) )
141, 13wceq 1632 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  27319  frlmrcl  27328
  Copyright terms: Public domain W3C validator