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	⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
	lidrideqd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
	lidrideqd.li	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐿 + 𝑥 ) = 𝑥 )
	lidrideqd.ri	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 )
	lidrideqd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	lidrideqd.p	⊢ + = ( +_g ‘ 𝐺 )
	lidrididd.o	⊢ 0 = ( 0_g ‘ 𝐺 )
Assertion	lidrididd	⊢ ( 𝜑 → 𝐿 = 0 )

Proof

Step	Hyp	Ref	Expression
1		lidrideqd.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
2		lidrideqd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
3		lidrideqd.li	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐿 + 𝑥 ) = 𝑥 )
4		lidrideqd.ri	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 )
5		lidrideqd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
6		lidrideqd.p	⊢ + = ( +_g ‘ 𝐺 )
7		lidrididd.o	⊢ 0 = ( 0_g ‘ 𝐺 )
8		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐿 + 𝑥 ) = ( 𝐿 + 𝑦 ) )
9		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
10	8 9	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐿 + 𝑥 ) = 𝑥 ↔ ( 𝐿 + 𝑦 ) = 𝑦 ) )
11	10	rspcv	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐿 + 𝑥 ) = 𝑥 → ( 𝐿 + 𝑦 ) = 𝑦 ) )
12	3 11	mpan9	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐿 + 𝑦 ) = 𝑦 )
13	1 2 3 4	lidrideqd	⊢ ( 𝜑 → 𝐿 = 𝑅 )
14		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 𝑅 ) = ( 𝑦 + 𝑅 ) )
15	14 9	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 + 𝑅 ) = 𝑥 ↔ ( 𝑦 + 𝑅 ) = 𝑦 ) )
16	15	rspcv	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 → ( 𝑦 + 𝑅 ) = 𝑦 ) )
17		oveq2	⊢ ( 𝐿 = 𝑅 → ( 𝑦 + 𝐿 ) = ( 𝑦 + 𝑅 ) )
18	17	adantl	⊢ ( ( ( 𝑦 + 𝑅 ) = 𝑦 ∧ 𝐿 = 𝑅 ) → ( 𝑦 + 𝐿 ) = ( 𝑦 + 𝑅 ) )
19		simpl	⊢ ( ( ( 𝑦 + 𝑅 ) = 𝑦 ∧ 𝐿 = 𝑅 ) → ( 𝑦 + 𝑅 ) = 𝑦 )
20	18 19	eqtrd	⊢ ( ( ( 𝑦 + 𝑅 ) = 𝑦 ∧ 𝐿 = 𝑅 ) → ( 𝑦 + 𝐿 ) = 𝑦 )
21	20	ex	⊢ ( ( 𝑦 + 𝑅 ) = 𝑦 → ( 𝐿 = 𝑅 → ( 𝑦 + 𝐿 ) = 𝑦 ) )
22	16 21	syl6com	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 → ( 𝑦 ∈ 𝐵 → ( 𝐿 = 𝑅 → ( 𝑦 + 𝐿 ) = 𝑦 ) ) )
23	22	com23	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 → ( 𝐿 = 𝑅 → ( 𝑦 ∈ 𝐵 → ( 𝑦 + 𝐿 ) = 𝑦 ) ) )
24	4 13 23	sylc	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑦 + 𝐿 ) = 𝑦 ) )
25	24	imp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 + 𝐿 ) = 𝑦 )
26	5 7 6 1 12 25	ismgmid2	⊢ ( 𝜑 → 𝐿 = 0 )

Metamath Proof Explorer

Theorem lidrididd

Proof