Theorem grpidd2

Description: Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd . (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	grpidd2.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	grpidd2.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	grpidd2.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
	grpidd2.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
	grpidd2.j	$$⊢\phi \to G\in \mathrm{Grp}$$
Assertion	grpidd2	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$

Proof

Step	Hyp	Ref	Expression
1		grpidd2.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		grpidd2.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		grpidd2.z	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
4		grpidd2.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
5		grpidd2.j	$$⊢\phi \to G\in \mathrm{Grp}$$
6	2	oveqd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}$$
7		oveq2	$$⊢x=\underset{\dot{}}{0}\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=\underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}$$
8		id	$$⊢x=\underset{\dot{}}{0}\to x=\underset{\dot{}}{0}$$
9	7 8	eqeq12d	$$⊢x=\underset{\dot{}}{0}\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
10	4	ralrimiva	$$⊢\phi \to \forall x\in B\underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
11	9 10 3	rspcdva	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
12	6 11	eqtr3d	$$⊢\phi \to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	3 1	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
14		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
15		eqid	$$⊢{+}_G={+}_G$$
16		eqid	$$⊢0_G=0_G$$
17	14 15 16	grpid	$$⊢\left(G\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}\leftrightarrow 0_G=\underset{\dot{}}{0}\right)$$
18	5 13 17	syl2anc	$$⊢\phi \to \left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}\leftrightarrow 0_G=\underset{\dot{}}{0}\right)$$
19	12 18	mpbid	$$⊢\phi \to 0_G=\underset{\dot{}}{0}$$
20	19	eqcomd	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$