Theorem ringinvdv

Description: Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringinvdv.b	|- B = ( Base ` R )
	ringinvdv.u	|- U = ( Unit ` R )
	ringinvdv.d	|- ./ = ( /r ` R )
	ringinvdv.o	|- .1. = ( 1r ` R )
	ringinvdv.i	|- I = ( invr ` R )
Assertion	ringinvdv	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) )

Proof

Step	Hyp	Ref	Expression
1		ringinvdv.b	|- B = ( Base ` R )
2		ringinvdv.u	|- U = ( Unit ` R )
3		ringinvdv.d	|- ./ = ( /r ` R )
4		ringinvdv.o	|- .1. = ( 1r ` R )
5		ringinvdv.i	|- I = ( invr ` R )
6	1 4	ringidcl	|- ( R e. Ring -> .1. e. B )
7		eqid	|- ( .r ` R ) = ( .r ` R )
8	1 7 2 5 3	dvrval	|- ( ( .1. e. B /\ X e. U ) -> ( .1. ./ X ) = ( .1. ( .r ` R ) ( I ` X ) ) )
9	6 8	sylan	|- ( ( R e. Ring /\ X e. U ) -> ( .1. ./ X ) = ( .1. ( .r ` R ) ( I ` X ) ) )
10	2 5 1	ringinvcl	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B )
11	1 7 4	ringlidm	|- ( ( R e. Ring /\ ( I ` X ) e. B ) -> ( .1. ( .r ` R ) ( I ` X ) ) = ( I ` X ) )
12	10 11	syldan	|- ( ( R e. Ring /\ X e. U ) -> ( .1. ( .r ` R ) ( I ` X ) ) = ( I ` X ) )
13	9 12	eqtr2d	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) )