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	$$⊢\phi \to B={\mathrm{Base}}_G$$
	grpidd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	grpidd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
	grpidd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
	grpidd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x$$
Assertion	grpidd	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$

Proof

Step	Hyp	Ref	Expression
1		grpidd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		grpidd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		grpidd.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
4		grpidd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
5		grpidd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7		eqid	$$⊢0_G=0_G$$
8		eqid	$$⊢{+}_G={+}_G$$
9	3 1	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
10	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_G\right)$$
11	10	biimpar	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to x\in B$$
12	2	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{+}={+}_G$$
13	12	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=\underset{\dot{}}{0}{+}_{G}x$$
14	13 4	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}{+}_{G}x=x$$
15	11 14	syldan	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to \underset{\dot{}}{0}{+}_{G}x=x$$
16	12	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x{+}_G\underset{\dot{}}{0}$$
17	16 5	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to x{+}_G\underset{\dot{}}{0}=x$$
18	11 17	syldan	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_G\right)\to x{+}_G\underset{\dot{}}{0}=x$$
19	6 7 8 9 15 18	ismgmid2	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$