Theorem dvrid

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

	Ref	Expression
Hypotheses	unitdvcl.o	|- U = ( Unit ` R )
	unitdvcl.d	|- ./ = ( /r ` R )
	dvrid.o	|- .1. = ( 1r ` R )
Assertion	dvrid	|- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		unitdvcl.o	|- U = ( Unit ` R )
2		unitdvcl.d	|- ./ = ( /r ` R )
3		dvrid.o	|- .1. = ( 1r ` R )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	4 1	unitcl	|- ( X e. U -> X e. ( Base ` R ) )
6	5	adantl	|- ( ( R e. Ring /\ X e. U ) -> X e. ( Base ` R ) )
7		eqid	|- ( .r ` R ) = ( .r ` R )
8		eqid	|- ( invr ` R ) = ( invr ` R )
9	4 7 1 8 2	dvrval	|- ( ( X e. ( Base ` R ) /\ X e. U ) -> ( X ./ X ) = ( X ( .r ` R ) ( ( invr ` R ) ` X ) ) )
10	6 9	sylancom	|- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = ( X ( .r ` R ) ( ( invr ` R ) ` X ) ) )
11	1 8 7 3	unitrinv	|- ( ( R e. Ring /\ X e. U ) -> ( X ( .r ` R ) ( ( invr ` R ) ` X ) ) = .1. )
12	10 11	eqtrd	|- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = .1. )