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	$$⊢\mathrm{ringLMod}=\left(w\in \mathrm{V}⟼\mathrm{subringAlg}\left(w\right)\left({\mathrm{Base}}_w\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crglmod	$$class\mathrm{ringLMod}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		csra	$$class\mathrm{subringAlg}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class\mathrm{subringAlg}\left(w\right)$$
6		cbs	$$class\mathrm{Base}$$
7	4 6	cfv	$$class{\mathrm{Base}}_w$$
8	7 5	cfv	$$class\mathrm{subringAlg}\left(w\right)\left({\mathrm{Base}}_w\right)$$
9	1 2 8	cmpt	$$class\left(w\in \mathrm{V}⟼\mathrm{subringAlg}\left(w\right)\left({\mathrm{Base}}_w\right)\right)$$
10	0 9	wceq	$$wff\mathrm{ringLMod}=\left(w\in \mathrm{V}⟼\mathrm{subringAlg}\left(w\right)\left({\mathrm{Base}}_w\right)\right)$$