Step |
Hyp |
Ref |
Expression |
1 |
|
ringinvdv.b |
|- B = ( Base ` R ) |
2 |
|
ringinvdv.u |
|- U = ( Unit ` R ) |
3 |
|
ringinvdv.d |
|- ./ = ( /r ` R ) |
4 |
|
ringinvdv.o |
|- .1. = ( 1r ` R ) |
5 |
|
ringinvdv.i |
|- I = ( invr ` R ) |
6 |
1 4
|
ringidcl |
|- ( R e. Ring -> .1. e. B ) |
7 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
8 |
1 7 2 5 3
|
dvrval |
|- ( ( .1. e. B /\ X e. U ) -> ( .1. ./ X ) = ( .1. ( .r ` R ) ( I ` X ) ) ) |
9 |
6 8
|
sylan |
|- ( ( R e. Ring /\ X e. U ) -> ( .1. ./ X ) = ( .1. ( .r ` R ) ( I ` X ) ) ) |
10 |
2 5 1
|
ringinvcl |
|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B ) |
11 |
1 7 4
|
ringlidm |
|- ( ( R e. Ring /\ ( I ` X ) e. B ) -> ( .1. ( .r ` R ) ( I ` X ) ) = ( I ` X ) ) |
12 |
10 11
|
syldan |
|- ( ( R e. Ring /\ X e. U ) -> ( .1. ( .r ` R ) ( I ` X ) ) = ( I ` X ) ) |
13 |
9 12
|
eqtr2d |
|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) ) |