Theorem mgmlrid

Description: The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ismgmid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ismgmid.o	⊢ 0 = ( 0g ‘ 𝐺 )
	ismgmid.p	⊢ + = ( +g ‘ 𝐺 )
	mgmidcl.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
Assertion	mgmlrid	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ismgmid.o	⊢ 0 = ( 0g ‘ 𝐺 )
3		ismgmid.p	⊢ + = ( +g ‘ 𝐺 )
4		mgmidcl.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
5		eqid	⊢ 0 = 0
6	1 2 3 4	ismgmid	⊢ ( 𝜑 → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ↔ 0 = 0 ) )
7	5 6	mpbiri	⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) )
8	7	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) )
9		oveq2	⊢ ( 𝑥 = 𝑋 → ( 0 + 𝑥 ) = ( 0 + 𝑋 ) )
10		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
11	9 10	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 0 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑋 ) = 𝑋 ) )
12		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 + 0 ) = ( 𝑋 + 0 ) )
13	12 10	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 0 ) = 𝑥 ↔ ( 𝑋 + 0 ) = 𝑋 ) )
14	11 13	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ↔ ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) )
15	14	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) )
16	8 15	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) )