Definition df-lidl

Description: Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. For the usual textbook definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring, see dflidl2rng and dflidl2 . (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	df-lidl	$$⊢\mathrm{LIdeal}=\mathrm{LSubSp}\circ \mathrm{ringLMod}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clidl	$$class\mathrm{LIdeal}$$
1		clss	$$class\mathrm{LSubSp}$$
2		crglmod	$$class\mathrm{ringLMod}$$
3	1 2	ccom	$$class\left(\mathrm{LSubSp}\circ \mathrm{ringLMod}\right)$$
4	0 3	wceq	$$wff\mathrm{LIdeal}=\mathrm{LSubSp}\circ \mathrm{ringLMod}$$