Theorem lidrididd

Description: If there is a left and right identity element for any binary operation (group operation) .+ , the left identity element (and therefore also the right identity element according to lidrideqd ) is equal to the two-sided identity element. (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$$
	lidrideqd.b	$$⊢B={\mathrm{Base}}_G$$
	lidrideqd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	lidrididd.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	lidrididd	$$⊢\phi \to L=\underset{\dot{}}{0}$$

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		lidrideqd.b	$$⊢B={\mathrm{Base}}_G$$
6		lidrideqd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
7		lidrididd.o	$$⊢\underset{\dot{}}{0}=0_G$$
8		oveq2	$$⊢x=y\to L\underset{\dot{}}{+}x=L\underset{\dot{}}{+}y$$
9		id	$$⊢x=y\to x=y$$
10	8 9	eqeq12d	$$⊢x=y\to \left(L\underset{\dot{}}{+}x=x\leftrightarrow L\underset{\dot{}}{+}y=y\right)$$
11	10	rspcv	$$⊢y\in B\to \left(\forall x\in BL\underset{\dot{}}{+}x=x\to L\underset{\dot{}}{+}y=y\right)$$
12	3 11	mpan9	$$⊢\left(\phi \wedge y\in B\right)\to L\underset{\dot{}}{+}y=y$$
13	1 2 3 4	lidrideqd	$$⊢\phi \to L=R$$
14		oveq1	$$⊢x=y\to x\underset{\dot{}}{+}R=y\underset{\dot{}}{+}R$$
15	14 9	eqeq12d	$$⊢x=y\to \left(x\underset{\dot{}}{+}R=x\leftrightarrow y\underset{\dot{}}{+}R=y\right)$$
16	15	rspcv	$$⊢y\in B\to \left(\forall x\in Bx\underset{\dot{}}{+}R=x\to y\underset{\dot{}}{+}R=y\right)$$
17		oveq2	$$⊢L=R\to y\underset{\dot{}}{+}L=y\underset{\dot{}}{+}R$$
18	17	adantl	$$⊢\left(y\underset{\dot{}}{+}R=y\wedge L=R\right)\to y\underset{\dot{}}{+}L=y\underset{\dot{}}{+}R$$
19		simpl	$$⊢\left(y\underset{\dot{}}{+}R=y\wedge L=R\right)\to y\underset{\dot{}}{+}R=y$$
20	18 19	eqtrd	$$⊢\left(y\underset{\dot{}}{+}R=y\wedge L=R\right)\to y\underset{\dot{}}{+}L=y$$
21	20	ex	$$⊢y\underset{\dot{}}{+}R=y\to \left(L=R\to y\underset{\dot{}}{+}L=y\right)$$
22	16 21	syl6com	$$⊢\forall x\in Bx\underset{\dot{}}{+}R=x\to \left(y\in B\to \left(L=R\to y\underset{\dot{}}{+}L=y\right)\right)$$
23	22	com23	$$⊢\forall x\in Bx\underset{\dot{}}{+}R=x\to \left(L=R\to \left(y\in B\to y\underset{\dot{}}{+}L=y\right)\right)$$
24	4 13 23	sylc	$$⊢\phi \to \left(y\in B\to y\underset{\dot{}}{+}L=y\right)$$
25	24	imp	$$⊢\left(\phi \wedge y\in B\right)\to y\underset{\dot{}}{+}L=y$$
26	5 7 6 1 12 25	ismgmid2	$$⊢\phi \to L=\underset{\dot{}}{0}$$