Definition df-frlm 18538

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

Step	Hyp	Ref	Expression
1		cfrlm 18537	. 2 class freeLMod
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 3106	. . 3 class _V
5	2	cv 1373	. . . 4 class r
6	3	cv 1373	. . . . 5 class i
7		crglmod 17591	. . . . . . 7 class ringLMod
8	5, 7	cfv 5579	. . . . . 6 class (ringLMod ` r )
9	8	csn 4020	. . . . 5 class { (ringLMod ` r ) }
10	6, 9	cxp 4990	. . . 4 class ( i X. { (ringLMod ` r ) } )
11		cdsmm 18522	. . . 4 class (+)m
12	5, 10, 11	co 6275	. . 3 class ( r (+)m ( i X. { (ringLMod ` r ) } ) )
13	2, 3, 4, 4, 12	cmpt2 6277	. 2 class ( r e. _V , i e. _V |-> ( r (+)m ( i X. { (ringLMod ` r ) } ) ) )
14	1, 13	wceq 1374	1 wff freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { (ringLMod ` r ) } ) ) )

This definition is referenced by:  frlmval  18539  frlmrcl  18550