This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 | ⊢ LIdeal = ( LSubSp ∘ ringLMod ) |
| 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 ) |