Description: Alternate (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. (Contributed by AV, 13-Feb-2025) (Proof shortened by AV, 18-Apr-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dflidl2.u | |- U = ( LIdeal ` R ) |
|
| dflidl2.b | |- B = ( Base ` R ) |
||
| dflidl2.t | |- .x. = ( .r ` R ) |
||
| Assertion | dflidl2 | |- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dflidl2.u | |- U = ( LIdeal ` R ) |
|
| 2 | dflidl2.b | |- B = ( Base ` R ) |
|
| 3 | dflidl2.t | |- .x. = ( .r ` R ) |
|
| 4 | 1 | lidlsubg | |- ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) ) |
| 5 | ringrng | |- ( R e. Ring -> R e. Rng ) |
|
| 6 | 1 2 3 | dflidl2rng | |- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x .x. y ) e. I ) ) |
| 7 | 5 6 | sylan | |- ( ( R e. Ring /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x .x. y ) e. I ) ) |
| 8 | 4 7 | biadanid | |- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) ) |