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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdrng4.0	⊢ 0 = ( 0g ‘ 𝑅 )
	isdrng4.1	⊢ 1 = ( 1r ‘ 𝑅 )
	isdrng4.x	⊢ · = ( .r ‘ 𝑅 )
	isdrng4.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	isdrng4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ringinveu.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ringinveu.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ringinveu.3	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	ringinveu.4	⊢ ( 𝜑 → ( 𝑌 · 𝑋 ) = 1 )
	ringinveu.5	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = 1 )
Assertion	ringinveu	⊢ ( 𝜑 → 𝑍 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		isdrng4.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdrng4.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		isdrng4.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		isdrng4.x	⊢ · = ( .r ‘ 𝑅 )
5		isdrng4.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
6		isdrng4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		ringinveu.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		ringinveu.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		ringinveu.3	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10		ringinveu.4	⊢ ( 𝜑 → ( 𝑌 · 𝑋 ) = 1 )
11		ringinveu.5	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = 1 )
12	11	oveq2d	⊢ ( 𝜑 → ( 𝑌 · ( 𝑋 · 𝑍 ) ) = ( 𝑌 · 1 ) )
13	10	oveq1d	⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) · 𝑍 ) = ( 1 · 𝑍 ) )
14	1 4 6 8 7 9	ringassd	⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) · 𝑍 ) = ( 𝑌 · ( 𝑋 · 𝑍 ) ) )
15	1 4 3 6 9	ringlidmd	⊢ ( 𝜑 → ( 1 · 𝑍 ) = 𝑍 )
16	13 14 15	3eqtr3d	⊢ ( 𝜑 → ( 𝑌 · ( 𝑋 · 𝑍 ) ) = 𝑍 )
17	1 4 3 6 8	ringridmd	⊢ ( 𝜑 → ( 𝑌 · 1 ) = 𝑌 )
18	12 16 17	3eqtr3d	⊢ ( 𝜑 → 𝑍 = 𝑌 )