MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-frlm Structured version   Visualization version   GIF version

Definition df-frlm 19848
Description: The 𝑖-dimensional free module over a ring 𝑟 is the product of 𝑖-many copies of the ring with componentwise addition and multiplication. If 𝑖 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 = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑟m (𝑖 × {(ringLMod‘𝑟)})))
Distinct variable group:   𝑖,𝑟

Detailed syntax breakdown of Definition df-frlm
StepHypRef Expression
1 cfrlm 19847 . 2 class freeLMod
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3168 . . 3 class V
52cv 1473 . . . 4 class 𝑟
63cv 1473 . . . . 5 class 𝑖
7 crglmod 18932 . . . . . . 7 class ringLMod
85, 7cfv 5786 . . . . . 6 class (ringLMod‘𝑟)
98csn 4120 . . . . 5 class {(ringLMod‘𝑟)}
106, 9cxp 5022 . . . 4 class (𝑖 × {(ringLMod‘𝑟)})
11 cdsmm 19832 . . . 4 class m
125, 10, 11co 6523 . . 3 class (𝑟m (𝑖 × {(ringLMod‘𝑟)}))
132, 3, 4, 4, 12cmpt2 6525 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑟m (𝑖 × {(ringLMod‘𝑟)})))
141, 13wceq 1474 1 wff freeLMod = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑟m (𝑖 × {(ringLMod‘𝑟)})))
Colors of variables: wff setvar class
This definition is referenced by:  frlmval  19849  frlmrcl  19858
  Copyright terms: Public domain W3C validator