Step |
Hyp |
Ref |
Expression |
1 |
|
opprbas.1 |
|- O = ( oppR ` R ) |
2 |
|
ringrng |
|- ( R e. Ring -> R e. Rng ) |
3 |
1
|
opprrng |
|- ( R e. Rng -> O e. Rng ) |
4 |
2 3
|
syl |
|- ( R e. Ring -> O e. Rng ) |
5 |
|
oveq1 |
|- ( z = ( 1r ` R ) -> ( z ( .r ` O ) x ) = ( ( 1r ` R ) ( .r ` O ) x ) ) |
6 |
5
|
eqeq1d |
|- ( z = ( 1r ` R ) -> ( ( z ( .r ` O ) x ) = x <-> ( ( 1r ` R ) ( .r ` O ) x ) = x ) ) |
7 |
6
|
ovanraleqv |
|- ( z = ( 1r ` R ) -> ( A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) <-> A. x e. ( Base ` R ) ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) ) ) |
8 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
9 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
10 |
8 9
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) ) |
11 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
12 |
|
eqid |
|- ( .r ` O ) = ( .r ` O ) |
13 |
8 11 1 12
|
opprmul |
|- ( ( 1r ` R ) ( .r ` O ) x ) = ( x ( .r ` R ) ( 1r ` R ) ) |
14 |
8 11 9
|
ringridm |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 1r ` R ) ) = x ) |
15 |
13 14
|
eqtrid |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` O ) x ) = x ) |
16 |
8 11 1 12
|
opprmul |
|- ( x ( .r ` O ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) x ) |
17 |
8 11 9
|
ringlidm |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) |
18 |
16 17
|
eqtrid |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` O ) ( 1r ` R ) ) = x ) |
19 |
15 18
|
jca |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) ) |
20 |
19
|
ralrimiva |
|- ( R e. Ring -> A. x e. ( Base ` R ) ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) ) |
21 |
7 10 20
|
rspcedvdw |
|- ( R e. Ring -> E. z e. ( Base ` R ) A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) ) |
22 |
1 8
|
opprbas |
|- ( Base ` R ) = ( Base ` O ) |
23 |
22 12
|
isringrng |
|- ( O e. Ring <-> ( O e. Rng /\ E. z e. ( Base ` R ) A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) ) ) |
24 |
4 21 23
|
sylanbrc |
|- ( R e. Ring -> O e. Ring ) |