1rinv

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

	Ref	Expression
Hypotheses	1rinv.1	$⊢ I = {inv}_{r} (R)$
	1rinv.2	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	1rinv	$⊢ R \in Ring \to I (\underset{˙}{1}) = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		1rinv.1	$⊢ I = {inv}_{r} (R)$
2		1rinv.2	$⊢ \underset{˙}{1} = 1_{R}$
3		eqid	$⊢ Unit (R) = Unit (R)$
4	3 2	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in Unit (R)$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	3 1 5	ringinvcl	$⊢ (R \in Ring \land \underset{˙}{1} \in Unit (R)) \to I (\underset{˙}{1}) \in {Base}_{R}$
7	4 6	mpdan	$⊢ R \in Ring \to I (\underset{˙}{1}) \in {Base}_{R}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9	5 8 2	ringlidm	$⊢ (R \in Ring \land I (\underset{˙}{1}) \in {Base}_{R}) \to \underset{˙}{1} \cdot_{R} I (\underset{˙}{1}) = I (\underset{˙}{1})$
10	7 9	mpdan	$⊢ R \in Ring \to \underset{˙}{1} \cdot_{R} I (\underset{˙}{1}) = I (\underset{˙}{1})$
11	3 1 8 2	unitrinv	$⊢ (R \in Ring \land \underset{˙}{1} \in Unit (R)) \to \underset{˙}{1} \cdot_{R} I (\underset{˙}{1}) = \underset{˙}{1}$
12	4 11	mpdan	$⊢ R \in Ring \to \underset{˙}{1} \cdot_{R} I (\underset{˙}{1}) = \underset{˙}{1}$
13	10 12	eqtr3d	$⊢ R \in Ring \to I (\underset{˙}{1}) = \underset{˙}{1}$

Metamath Proof Explorer