Definition df-rgmod

Description: Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014)

	Ref	Expression
Assertion	df-rgmod	⊢ ringLMod = ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crglmod	⊢ ringLMod
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		csra	⊢ subringAlg
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( subringAlg ‘ 𝑤 )
6		cbs	⊢ Base
7	4 6	cfv	⊢ ( Base ‘ 𝑤 )
8	7 5	cfv	⊢ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) )
9	1 2 8	cmpt	⊢ ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )
10	0 9	wceq	⊢ ringLMod = ( 𝑤 ∈ V ↦ ( ( subringAlg ‘ 𝑤 ) ‘ ( Base ‘ 𝑤 ) ) )