Metamath Proof Explorer

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 o. ringLMod )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clidl 
 |-  LIdeal
1 clss 
 |-  LSubSp
2 crglmod 
 |-  ringLMod
3 1 2 ccom 
 |-  ( LSubSp o. ringLMod )
4 0 3 wceq 
 |-  LIdeal = ( LSubSp o. ringLMod )