This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringinveu

Description: If a ring unit element X admits both a left inverse Y and a right inverse Z , they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025)

		Ref	Expression
	Hypotheses	isdrng4.b	$⊢ B = {Base}_{R}$
		isdrng4.0	$⊢ \underset{˙}{0} = 0_{R}$
		isdrng4.1	$⊢ \underset{˙}{1} = 1_{R}$
		isdrng4.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		isdrng4.u	$⊢ U = Unit (R)$
		isdrng4.r	$⊢ φ \to R \in Ring$
		ringinveu.1	$⊢ φ \to X \in B$
		ringinveu.2	$⊢ φ \to Y \in B$
		ringinveu.3	$⊢ φ \to Z \in B$
		ringinveu.4	$⊢ φ \to Y \underset{˙}{\cdot} X = \underset{˙}{1}$
		ringinveu.5	$⊢ φ \to X \underset{˙}{\cdot} Z = \underset{˙}{1}$
	Assertion	ringinveu	$⊢ φ \to Z = Y$

Proof

Step	Hyp	Ref	Expression
1		isdrng4.b	$⊢ B = {Base}_{R}$
2		isdrng4.0	$⊢ \underset{˙}{0} = 0_{R}$
3		isdrng4.1	$⊢ \underset{˙}{1} = 1_{R}$
4		isdrng4.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		isdrng4.u	$⊢ U = Unit (R)$
6		isdrng4.r	$⊢ φ \to R \in Ring$
7		ringinveu.1	$⊢ φ \to X \in B$
8		ringinveu.2	$⊢ φ \to Y \in B$
9		ringinveu.3	$⊢ φ \to Z \in B$
10		ringinveu.4	$⊢ φ \to Y \underset{˙}{\cdot} X = \underset{˙}{1}$
11		ringinveu.5	$⊢ φ \to X \underset{˙}{\cdot} Z = \underset{˙}{1}$
12	11	oveq2d	$⊢ φ \to Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z) = Y \underset{˙}{\cdot} \underset{˙}{1}$
13	10	oveq1d	$⊢ φ \to (Y \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = \underset{˙}{1} \underset{˙}{\cdot} Z$
14	1 4 6 8 7 9	ringassd	$⊢ φ \to (Y \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$
15	1 4 3 6 9	ringlidmd	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} Z = Z$
16	13 14 15	3eqtr3d	$⊢ φ \to Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z) = Z$
17	1 4 3 6 8	ringridmd	$⊢ φ \to Y \underset{˙}{\cdot} \underset{˙}{1} = Y$
18	12 16 17	3eqtr3d	$⊢ φ \to Z = Y$