Theorem grpidd

Description: Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpidd.b	|- ( ph -> B = ( Base ` G ) )
	grpidd.p	|- ( ph -> .+ = ( +g ` G ) )
	grpidd.z	|- ( ph -> .0. e. B )
	grpidd.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
	grpidd.j	|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
Assertion	grpidd	|- ( ph -> .0. = ( 0g ` G ) )

Proof

Step	Hyp	Ref	Expression
1		grpidd.b	|- ( ph -> B = ( Base ` G ) )
2		grpidd.p	|- ( ph -> .+ = ( +g ` G ) )
3		grpidd.z	|- ( ph -> .0. e. B )
4		grpidd.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
5		grpidd.j	|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
6		eqid	|- ( Base ` G ) = ( Base ` G )
7		eqid	|- ( 0g ` G ) = ( 0g ` G )
8		eqid	|- ( +g ` G ) = ( +g ` G )
9	3 1	eleqtrd	|- ( ph -> .0. e. ( Base ` G ) )
10	1	eleq2d	|- ( ph -> ( x e. B <-> x e. ( Base ` G ) ) )
11	10	biimpar	|- ( ( ph /\ x e. ( Base ` G ) ) -> x e. B )
12	2	adantr	|- ( ( ph /\ x e. B ) -> .+ = ( +g ` G ) )
13	12	oveqd	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = ( .0. ( +g ` G ) x ) )
14	13 4	eqtr3d	|- ( ( ph /\ x e. B ) -> ( .0. ( +g ` G ) x ) = x )
15	11 14	syldan	|- ( ( ph /\ x e. ( Base ` G ) ) -> ( .0. ( +g ` G ) x ) = x )
16	12	oveqd	|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = ( x ( +g ` G ) .0. ) )
17	16 5	eqtr3d	|- ( ( ph /\ x e. B ) -> ( x ( +g ` G ) .0. ) = x )
18	11 17	syldan	|- ( ( ph /\ x e. ( Base ` G ) ) -> ( x ( +g ` G ) .0. ) = x )
19	6 7 8 9 15 18	ismgmid2	|- ( ph -> .0. = ( 0g ` G ) )