Definition df-frlm

Description: Define the function associating with a ring and a set the direct sum indexed by that set of copies of that ring regarded as a left module over itself. Recall from df-dsmm that an element of a direct sum has finitely many nonzero coordinates. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	df-frlm	⊢ freeLMod = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrlm	⊢ freeLMod
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vi	⊢ 𝑖
4	1	cv	⊢ 𝑟
5		cdsmm	⊢ ⊕m
6	3	cv	⊢ 𝑖
7		crglmod	⊢ ringLMod
8	4 7	cfv	⊢ ( ringLMod ‘ 𝑟 )
9	8	csn	⊢ { ( ringLMod ‘ 𝑟 ) }
10	6 9	cxp	⊢ ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } )
11	4 10 5	co	⊢ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) )
12	1 3 2 2 11	cmpo	⊢ ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )
13	0 12	wceq	⊢ freeLMod = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )