Step |
Hyp |
Ref |
Expression |
1 |
|
ringunitnzdiv.b |
|- B = ( Base ` R ) |
2 |
|
ringunitnzdiv.z |
|- .0. = ( 0g ` R ) |
3 |
|
ringunitnzdiv.t |
|- .x. = ( .r ` R ) |
4 |
|
ringunitnzdiv.r |
|- ( ph -> R e. Ring ) |
5 |
|
ringunitnzdiv.y |
|- ( ph -> Y e. B ) |
6 |
|
ringunitnzdiv.x |
|- ( ph -> X e. ( Unit ` R ) ) |
7 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
8 |
|
eqid |
|- ( Unit ` R ) = ( Unit ` R ) |
9 |
1 8
|
unitcl |
|- ( X e. ( Unit ` R ) -> X e. B ) |
10 |
6 9
|
syl |
|- ( ph -> X e. B ) |
11 |
|
eqid |
|- ( invr ` R ) = ( invr ` R ) |
12 |
8 11 1
|
ringinvcl |
|- ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( ( invr ` R ) ` X ) e. B ) |
13 |
4 6 12
|
syl2anc |
|- ( ph -> ( ( invr ` R ) ` X ) e. B ) |
14 |
|
oveq1 |
|- ( e = ( ( invr ` R ) ` X ) -> ( e .x. X ) = ( ( ( invr ` R ) ` X ) .x. X ) ) |
15 |
14
|
eqeq1d |
|- ( e = ( ( invr ` R ) ` X ) -> ( ( e .x. X ) = ( 1r ` R ) <-> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) ) |
16 |
15
|
adantl |
|- ( ( ph /\ e = ( ( invr ` R ) ` X ) ) -> ( ( e .x. X ) = ( 1r ` R ) <-> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) ) |
17 |
8 11 3 7
|
unitlinv |
|- ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) |
18 |
4 6 17
|
syl2anc |
|- ( ph -> ( ( ( invr ` R ) ` X ) .x. X ) = ( 1r ` R ) ) |
19 |
13 16 18
|
rspcedvd |
|- ( ph -> E. e e. B ( e .x. X ) = ( 1r ` R ) ) |
20 |
1 3 7 2 4 10 19 5
|
ringinvnzdiv |
|- ( ph -> ( ( X .x. Y ) = .0. <-> Y = .0. ) ) |