Theorem 1rinv

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

	Ref	Expression
Hypotheses	1rinv.1	⊢ 𝐼 = ( invr ‘ 𝑅 )
	1rinv.2	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	1rinv	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ‘ 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1rinv.1	⊢ 𝐼 = ( invr ‘ 𝑅 )
2		1rinv.2	⊢ 1 = ( 1r ‘ 𝑅 )
3		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
4	3 2	1unit	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	3 1 5	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
7	4 6	mpdan	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9	5 8 2	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ 1 ) ∈ ( Base ‘ 𝑅 ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 1 ) ) = ( 𝐼 ‘ 1 ) )
10	7 9	mpdan	⊢ ( 𝑅 ∈ Ring → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 1 ) ) = ( 𝐼 ‘ 1 ) )
11	3 1 8 2	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Unit ‘ 𝑅 ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 1 ) ) = 1 )
12	4 11	mpdan	⊢ ( 𝑅 ∈ Ring → ( 1 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 1 ) ) = 1 )
13	10 12	eqtr3d	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ‘ 1 ) = 1 )