Description: A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2idllidld.1 | |- ( ph -> I e. ( 2Ideal ` R ) ) |
|
Assertion | 2idllidld | |- ( ph -> I e. ( LIdeal ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2idllidld.1 | |- ( ph -> I e. ( 2Ideal ` R ) ) |
|
2 | eqid | |- ( LIdeal ` R ) = ( LIdeal ` R ) |
|
3 | eqid | |- ( oppR ` R ) = ( oppR ` R ) |
|
4 | eqid | |- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) ) |
|
5 | eqid | |- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
|
6 | 2 3 4 5 | 2idlval | |- ( 2Ideal ` R ) = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) ) |
7 | 1 6 | eleqtrdi | |- ( ph -> I e. ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) ) ) |
8 | 7 | elin1d | |- ( ph -> I e. ( LIdeal ` R ) ) |