Theorem mgmidcl

Description: The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ismgmid.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ismgmid.o	⊢ 0 = ( 0g ‘ 𝐺 )
	ismgmid.p	⊢ + = ( +g ‘ 𝐺 )
	mgmidcl.e	⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )
Assertion	mgmidcl	⊢ ( 𝜑 → 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	simpld	⊢ ( 𝜑 → 0 ∈ 𝐵 )