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={\mathrm{Base}}_R$$
	isdrng4.0	$$⊢\underset{\dot{}}{0}=0_R$$
	isdrng4.1	$$⊢\underset{\dot{}}{1}=1_R$$
	isdrng4.x	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isdrng4.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	isdrng4.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringinveu.1	$$⊢\phi \to X\in B$$
	ringinveu.2	$$⊢\phi \to Y\in B$$
	ringinveu.3	$$⊢\phi \to Z\in B$$
	ringinveu.4	$$⊢\phi \to Y\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
	ringinveu.5	$$⊢\phi \to X\underset{\dot{}}{·}Z=\underset{\dot{}}{1}$$
Assertion	ringinveu	$$⊢\phi \to Z=Y$$

Proof

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