Theorem lidrideqd

Description: If there is a left and right identity element for any binary operation (group operation) .+ , both identity elements are equal. Generalization of statement in Lang p. 3: it is sufficient that "e" is a left identity element and "e``" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	lidrideqd.l	|- ( ph -> L e. B )
	lidrideqd.r	|- ( ph -> R e. B )
	lidrideqd.li	|- ( ph -> A. x e. B ( L .+ x ) = x )
	lidrideqd.ri	|- ( ph -> A. x e. B ( x .+ R ) = x )
Assertion	lidrideqd	|- ( ph -> L = R )

Proof

Step	Hyp	Ref	Expression
1		lidrideqd.l	|- ( ph -> L e. B )
2		lidrideqd.r	|- ( ph -> R e. B )
3		lidrideqd.li	|- ( ph -> A. x e. B ( L .+ x ) = x )
4		lidrideqd.ri	|- ( ph -> A. x e. B ( x .+ R ) = x )
5		oveq1	|- ( x = L -> ( x .+ R ) = ( L .+ R ) )
6		id	|- ( x = L -> x = L )
7	5 6	eqeq12d	|- ( x = L -> ( ( x .+ R ) = x <-> ( L .+ R ) = L ) )
8	7 4 1	rspcdva	|- ( ph -> ( L .+ R ) = L )
9		oveq2	|- ( x = R -> ( L .+ x ) = ( L .+ R ) )
10		id	|- ( x = R -> x = R )
11	9 10	eqeq12d	|- ( x = R -> ( ( L .+ x ) = x <-> ( L .+ R ) = R ) )
12	11 3 2	rspcdva	|- ( ph -> ( L .+ R ) = R )
13	8 12	eqtr3d	|- ( ph -> L = R )