Theorem dvreq1

Description: A cancellation law for division. ( 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	syl5ib	|- ( ( 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 ) )