Theorem 1rinv

Description: The inverse of the identity is the identity. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	1rinv.1	|- I = ( invr ` R )
	1rinv.2	|- .1. = ( 1r ` R )
Assertion	1rinv	|- ( R e. Ring -> ( I ` .1. ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		1rinv.1	|- I = ( invr ` R )
2		1rinv.2	|- .1. = ( 1r ` R )
3		eqid	|- ( Unit ` R ) = ( Unit ` R )
4	3 2	1unit	|- ( R e. Ring -> .1. e. ( Unit ` R ) )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	3 1 5	ringinvcl	|- ( ( R e. Ring /\ .1. e. ( Unit ` R ) ) -> ( I ` .1. ) e. ( Base ` R ) )
7	4 6	mpdan	|- ( R e. Ring -> ( I ` .1. ) e. ( Base ` R ) )
8		eqid	|- ( .r ` R ) = ( .r ` R )
9	5 8 2	ringlidm	|- ( ( R e. Ring /\ ( I ` .1. ) e. ( Base ` R ) ) -> ( .1. ( .r ` R ) ( I ` .1. ) ) = ( I ` .1. ) )
10	7 9	mpdan	|- ( R e. Ring -> ( .1. ( .r ` R ) ( I ` .1. ) ) = ( I ` .1. ) )
11	3 1 8 2	unitrinv	|- ( ( R e. Ring /\ .1. e. ( Unit ` R ) ) -> ( .1. ( .r ` R ) ( I ` .1. ) ) = .1. )
12	4 11	mpdan	|- ( R e. Ring -> ( .1. ( .r ` R ) ( I ` .1. ) ) = .1. )
13	10 12	eqtr3d	|- ( R e. Ring -> ( I ` .1. ) = .1. )