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	|- .0. = ( 0g ` R )
	isdrng4.1	|- .1. = ( 1r ` R )
	isdrng4.x	|- .x. = ( .r ` R )
	isdrng4.u	|- U = ( Unit ` R )
	isdrng4.r	|- ( ph -> R e. Ring )
	ringinveu.1	|- ( ph -> X e. B )
	ringinveu.2	|- ( ph -> Y e. B )
	ringinveu.3	|- ( ph -> Z e. B )
	ringinveu.4	|- ( ph -> ( Y .x. X ) = .1. )
	ringinveu.5	|- ( ph -> ( X .x. Z ) = .1. )
Assertion	ringinveu	|- ( ph -> Z = Y )

Proof

Step	Hyp	Ref	Expression
1		isdrng4.b	|- B = ( Base ` R )
2		isdrng4.0	|- .0. = ( 0g ` R )
3		isdrng4.1	|- .1. = ( 1r ` R )
4		isdrng4.x	|- .x. = ( .r ` R )
5		isdrng4.u	|- U = ( Unit ` R )
6		isdrng4.r	|- ( ph -> R e. Ring )
7		ringinveu.1	|- ( ph -> X e. B )
8		ringinveu.2	|- ( ph -> Y e. B )
9		ringinveu.3	|- ( ph -> Z e. B )
10		ringinveu.4	|- ( ph -> ( Y .x. X ) = .1. )
11		ringinveu.5	|- ( ph -> ( X .x. Z ) = .1. )
12	11	oveq2d	|- ( ph -> ( Y .x. ( X .x. Z ) ) = ( Y .x. .1. ) )
13	10	oveq1d	|- ( ph -> ( ( Y .x. X ) .x. Z ) = ( .1. .x. Z ) )
14	1 4 6 8 7 9	ringassd	|- ( ph -> ( ( Y .x. X ) .x. Z ) = ( Y .x. ( X .x. Z ) ) )
15	1 4 3 6 9	ringlidmd	|- ( ph -> ( .1. .x. Z ) = Z )
16	13 14 15	3eqtr3d	|- ( ph -> ( Y .x. ( X .x. Z ) ) = Z )
17	1 4 3 6 8	ringridmd	|- ( ph -> ( Y .x. .1. ) = Y )
18	12 16 17	3eqtr3d	|- ( ph -> Z = Y )