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	$$⊢\phi \to L\in B$$
	lidrideqd.r	$$⊢\phi \to R\in B$$
	lidrideqd.li	$$⊢\phi \to \forall x\in BL\underset{\dot{}}{+}x=x$$
	lidrideqd.ri	$$⊢\phi \to \forall x\in Bx\underset{\dot{}}{+}R=x$$
Assertion	lidrideqd	$$⊢\phi \to L=R$$

Proof

Step	Hyp	Ref	Expression
1		lidrideqd.l	$$⊢\phi \to L\in B$$
2		lidrideqd.r	$$⊢\phi \to R\in B$$
3		lidrideqd.li	$$⊢\phi \to \forall x\in BL\underset{\dot{}}{+}x=x$$
4		lidrideqd.ri	$$⊢\phi \to \forall x\in Bx\underset{\dot{}}{+}R=x$$
5		oveq1	$$⊢x=L\to x\underset{\dot{}}{+}R=L\underset{\dot{}}{+}R$$
6		id	$$⊢x=L\to x=L$$
7	5 6	eqeq12d	$$⊢x=L\to \left(x\underset{\dot{}}{+}R=x\leftrightarrow L\underset{\dot{}}{+}R=L\right)$$
8	7 4 1	rspcdva	$$⊢\phi \to L\underset{\dot{}}{+}R=L$$
9		oveq2	$$⊢x=R\to L\underset{\dot{}}{+}x=L\underset{\dot{}}{+}R$$
10		id	$$⊢x=R\to x=R$$
11	9 10	eqeq12d	$$⊢x=R\to \left(L\underset{\dot{}}{+}x=x\leftrightarrow L\underset{\dot{}}{+}R=R\right)$$
12	11 3 2	rspcdva	$$⊢\phi \to L\underset{\dot{}}{+}R=R$$
13	8 12	eqtr3d	$$⊢\phi \to L=R$$