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 = ( w e. _V |-> ( ( subringAlg ` w ) ` ( Base ` w ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crglmod	|- ringLMod
1		vw	|- w
2		cvv	|- _V
3		csra	|- subringAlg
4	1	cv	|- w
5	4 3	cfv	|- ( subringAlg ` w )
6		cbs	|- Base
7	4 6	cfv	|- ( Base ` w )
8	7 5	cfv	|- ( ( subringAlg ` w ) ` ( Base ` w ) )
9	1 2 8	cmpt	|- ( w e. _V |-> ( ( subringAlg ` w ) ` ( Base ` w ) ) )
10	0 9	wceq	|- ringLMod = ( w e. _V |-> ( ( subringAlg ` w ) ` ( Base ` w ) ) )