Definition df-frlm 19910

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

Step	Hyp	Ref	Expression
1		cfrlm 19909	. 2 class freeLMod
2		vr	. . 3 setvar 𝑟
3		vi	. . 3 setvar 𝑖
4		cvv 3173	. . 3 class V
5	2	cv 1474	. . . 4 class 𝑟
6	3	cv 1474	. . . . 5 class 𝑖
7		crglmod 18990	. . . . . . 7 class ringLMod
8	5, 7	cfv 5804	. . . . . 6 class (ringLMod‘𝑟)
9	8	csn 4125	. . . . 5 class {(ringLMod‘𝑟)}
10	6, 9	cxp 5036	. . . 4 class (𝑖 × {(ringLMod‘𝑟)})
11		cdsmm 19894	. . . 4 class ⊕m
12	5, 10, 11	co 6549	. . 3 class (𝑟 ⊕m (𝑖 × {(ringLMod‘𝑟)}))
13	2, 3, 4, 4, 12	cmpt2 6551	. 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑟 ⊕m (𝑖 × {(ringLMod‘𝑟)})))
14	1, 13	wceq 1475	1 wff freeLMod = (𝑟 ∈ V, 𝑖 ∈ V ↦ (𝑟 ⊕m (𝑖 × {(ringLMod‘𝑟)})))

This definition is referenced by:  frlmval  19911  frlmrcl  19920