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

Proof

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

Metamath Proof Explorer

Theorem lidrideqd

Proof