Step |
Hyp |
Ref |
Expression |
1 |
|
crng2idl.i |
|- I = ( LIdeal ` R ) |
2 |
|
inidm |
|- ( I i^i I ) = I |
3 |
|
eqid |
|- ( oppR ` R ) = ( oppR ` R ) |
4 |
1 3
|
crngridl |
|- ( R e. CRing -> I = ( LIdeal ` ( oppR ` R ) ) ) |
5 |
4
|
ineq2d |
|- ( R e. CRing -> ( I i^i I ) = ( I i^i ( LIdeal ` ( oppR ` R ) ) ) ) |
6 |
2 5
|
eqtr3id |
|- ( R e. CRing -> I = ( I i^i ( LIdeal ` ( oppR ` R ) ) ) ) |
7 |
|
eqid |
|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) ) |
8 |
|
eqid |
|- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
9 |
1 3 7 8
|
2idlval |
|- ( 2Ideal ` R ) = ( I i^i ( LIdeal ` ( oppR ` R ) ) ) |
10 |
6 9
|
eqtr4di |
|- ( R e. CRing -> I = ( 2Ideal ` R ) ) |