Theorem dvr1

Description: A cancellation law for division. ( div1 analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	dvr1.b	|- B = ( Base ` R )
	dvr1.d	|- ./ = ( /r ` R )
	dvr1.o	|- .1. = ( 1r ` R )
Assertion	dvr1	|- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )

Proof

Step	Hyp	Ref	Expression
1		dvr1.b	|- B = ( Base ` R )
2		dvr1.d	|- ./ = ( /r ` R )
3		dvr1.o	|- .1. = ( 1r ` R )
4		id	|- ( X e. B -> X e. B )
5		eqid	|- ( Unit ` R ) = ( Unit ` R )
6	5 3	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
7		eqid	|- ( .r ` R ) = ( .r ` R )
8		eqid	|- ( invr ` R ) = ( invr ` R )
9	1 7 5 8 2	dvrval	|- ( ( X e. B /\ .1. e. ( Unit ` R ) ) -> ( X ./ .1. ) = ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) )
10	4 6 9	syl2anr	|- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) )
11	8 3	1rinv	|- ( R e. Ring -> ( ( invr ` R ) ` .1. ) = .1. )
12	11	adantr	|- ( ( R e. Ring /\ X e. B ) -> ( ( invr ` R ) ` .1. ) = .1. )
13	12	oveq2d	|- ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) ( ( invr ` R ) ` .1. ) ) = ( X ( .r ` R ) .1. ) )
14	1 7 3	ringridm	|- ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .1. ) = X )
15	10 13 14	3eqtrd	|- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )