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	|- B = ( Base ` G )
	ismgmid.o	|- .0. = ( 0g ` G )
	ismgmid.p	|- .+ = ( +g ` G )
	mgmidcl.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
Assertion	mgmidcl	|- ( ph -> .0. e. B )

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	|- B = ( Base ` G )
2		ismgmid.o	|- .0. = ( 0g ` G )
3		ismgmid.p	|- .+ = ( +g ` G )
4		mgmidcl.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
5		eqid	|- .0. = .0.
6	1 2 3 4	ismgmid	|- ( ph -> ( ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) <-> .0. = .0. ) )
7	5 6	mpbiri	|- ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
8	7	simpld	|- ( ph -> .0. e. B )