Step |
Hyp |
Ref |
Expression |
1 |
|
rng2idlsubgsubrng.r |
|- ( ph -> R e. Rng ) |
2 |
|
rng2idlsubgsubrng.i |
|- ( ph -> I e. ( 2Ideal ` R ) ) |
3 |
|
rng2idlsubgsubrng.u |
|- ( ph -> I e. ( SubGrp ` R ) ) |
4 |
|
eqid |
|- ( LIdeal ` R ) = ( LIdeal ` R ) |
5 |
|
eqid |
|- ( oppR ` R ) = ( oppR ` R ) |
6 |
|
eqid |
|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) ) |
7 |
|
eqid |
|- ( 2Ideal ` R ) = ( 2Ideal ` R ) |
8 |
4 5 6 7
|
2idlelb |
|- ( I e. ( 2Ideal ` R ) <-> ( I e. ( LIdeal ` R ) /\ I e. ( LIdeal ` ( oppR ` R ) ) ) ) |
9 |
8
|
simplbi |
|- ( I e. ( 2Ideal ` R ) -> I e. ( LIdeal ` R ) ) |
10 |
2 9
|
syl |
|- ( ph -> I e. ( LIdeal ` R ) ) |
11 |
|
eqid |
|- ( R |`s I ) = ( R |`s I ) |
12 |
4 11
|
rnglidlrng |
|- ( ( R e. Rng /\ I e. ( LIdeal ` R ) /\ I e. ( SubGrp ` R ) ) -> ( R |`s I ) e. Rng ) |
13 |
1 10 3 12
|
syl3anc |
|- ( ph -> ( R |`s I ) e. Rng ) |
14 |
1 2 13
|
rng2idlsubrng |
|- ( ph -> I e. ( SubRng ` R ) ) |