Step |
Hyp |
Ref |
Expression |
1 |
|
dvrass.b |
|- B = ( Base ` R ) |
2 |
|
dvrass.o |
|- U = ( Unit ` R ) |
3 |
|
dvrass.d |
|- ./ = ( /r ` R ) |
4 |
|
dvrass.t |
|- .x. = ( .r ` R ) |
5 |
|
eqid |
|- ( invr ` R ) = ( invr ` R ) |
6 |
1 4 2 5 3
|
dvrval |
|- ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) ) |
7 |
6
|
3adant1 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) ) |
8 |
7
|
oveq1d |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) ) |
9 |
|
simp1 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> R e. Ring ) |
10 |
|
simp2 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> X e. B ) |
11 |
2 5 1
|
ringinvcl |
|- ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B ) |
12 |
11
|
3adant2 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B ) |
13 |
1 2
|
unitcl |
|- ( Y e. U -> Y e. B ) |
14 |
13
|
3ad2ant3 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> Y e. B ) |
15 |
1 4
|
ringass |
|- ( ( R e. Ring /\ ( X e. B /\ ( ( invr ` R ) ` Y ) e. B /\ Y e. B ) ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) ) |
16 |
9 10 12 14 15
|
syl13anc |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) ) |
17 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
18 |
2 5 4 17
|
unitlinv |
|- ( ( R e. Ring /\ Y e. U ) -> ( ( ( invr ` R ) ` Y ) .x. Y ) = ( 1r ` R ) ) |
19 |
18
|
3adant2 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( ( invr ` R ) ` Y ) .x. Y ) = ( 1r ` R ) ) |
20 |
19
|
oveq2d |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) = ( X .x. ( 1r ` R ) ) ) |
21 |
1 4 17
|
ringridm |
|- ( ( R e. Ring /\ X e. B ) -> ( X .x. ( 1r ` R ) ) = X ) |
22 |
21
|
3adant3 |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( 1r ` R ) ) = X ) |
23 |
20 22
|
eqtrd |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) = X ) |
24 |
16 23
|
eqtrd |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = X ) |
25 |
8 24
|
eqtrd |
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X ) |