This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvreq1

Description: Equality in terms of ratio equal to ring unity. ( diveq1 analog.) (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dvreq1.b 
|- B = ( Base ` R )
dvreq1.o 
|- U = ( Unit ` R )
dvreq1.d 
|- ./ = ( /r ` R )
dvreq1.t 
|- .1. = ( 1r ` R )
Assertion dvreq1 
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 dvreq1.b 
 |-  B = ( Base ` R )
2 dvreq1.o 
 |-  U = ( Unit ` R )
3 dvreq1.d 
 |-  ./ = ( /r ` R )
4 dvreq1.t 
 |-  .1. = ( 1r ` R )
5 oveq1 
 |-  ( ( X ./ Y ) = .1. -> ( ( X ./ Y ) ( .r ` R ) Y ) = ( .1. ( .r ` R ) Y ) )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 1 2 3 6 dvrcan1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) ( .r ` R ) Y ) = X )
8 1 2 unitcl 
 |-  ( Y e. U -> Y e. B )
9 1 6 4 ringlidm 
 |-  ( ( R e. Ring /\ Y e. B ) -> ( .1. ( .r ` R ) Y ) = Y )
10 8 9 sylan2 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( .1. ( .r ` R ) Y ) = Y )
11 10 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( .1. ( .r ` R ) Y ) = Y )
12 7 11 eqeq12d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( ( X ./ Y ) ( .r ` R ) Y ) = ( .1. ( .r ` R ) Y ) <-> X = Y ) )
13 5 12 imbitrid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. -> X = Y ) )
14 2 3 4 dvrid 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( Y ./ Y ) = .1. )
15 14 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( Y ./ Y ) = .1. )
16 oveq1 
 |-  ( X = Y -> ( X ./ Y ) = ( Y ./ Y ) )
17 16 eqeq1d 
 |-  ( X = Y -> ( ( X ./ Y ) = .1. <-> ( Y ./ Y ) = .1. ) )
18 15 17 syl5ibrcom 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X = Y -> ( X ./ Y ) = .1. ) )
19 13 18 impbid 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. <-> X = Y ) )