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. (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	df-lidl	⊢ LIdeal = ( LSubSp ∘ ringLMod )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clidl	⊢ LIdeal
1		clss	⊢ LSubSp
2		crglmod	⊢ ringLMod
3	1 2	ccom	⊢ ( LSubSp ∘ ringLMod )
4	0 3	wceq	⊢ LIdeal = ( LSubSp ∘ ringLMod )