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	$⊢ φ \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$
	lidrideqd.b	$⊢ B = {Base}_{G}$
	lidrideqd.p	$⊢ \underset{˙}{+} = +_{G}$
	lidrididd.o	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	lidrididd	$⊢ φ \to L = \underset{˙}{0}$

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

Metamath Proof Explorer

Theorem lidrididd

Proof