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	|- 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	mgmlrid	|- ( ( ph /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )

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	simprd	|- ( ph -> A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )
9		oveq2	|- ( x = X -> ( .0. .+ x ) = ( .0. .+ X ) )
10		id	|- ( x = X -> x = X )
11	9 10	eqeq12d	|- ( x = X -> ( ( .0. .+ x ) = x <-> ( .0. .+ X ) = X ) )
12		oveq1	|- ( x = X -> ( x .+ .0. ) = ( X .+ .0. ) )
13	12 10	eqeq12d	|- ( x = X -> ( ( x .+ .0. ) = x <-> ( X .+ .0. ) = X ) )
14	11 13	anbi12d	|- ( x = X -> ( ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) <-> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) ) )
15	14	rspccva	|- ( ( A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )
16	8 15	sylan	|- ( ( ph /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )