Theorem grpidval

Description: The value of the group identity element. (Contributed by NM, 20-Aug-2011) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	grpidval.b	$$⊢B={\mathrm{Base}}_G$$
	grpidval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpidval.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpidval	$$⊢\underset{\dot{}}{0}=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpidval.b	$$⊢B={\mathrm{Base}}_G$$
2		grpidval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpidval.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
5	4 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
6	5	eleq2d	$$⊢g=G\to \left(e\in {\mathrm{Base}}_g\leftrightarrow e\in B\right)$$
7		fveq2	$$⊢g=G\to {+}_g={+}_G$$
8	7 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
9	8	oveqd	$$⊢g=G\to e{+}_{g}x=e\underset{\dot{}}{+}x$$
10	9	eqeq1d	$$⊢g=G\to \left(e{+}_{g}x=x\leftrightarrow e\underset{\dot{}}{+}x=x\right)$$
11	8	oveqd	$$⊢g=G\to x{+}_{g}e=x\underset{\dot{}}{+}e$$
12	11	eqeq1d	$$⊢g=G\to \left(x{+}_{g}e=x\leftrightarrow x\underset{\dot{}}{+}e=x\right)$$
13	10 12	anbi12d	$$⊢g=G\to \left(\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\leftrightarrow \left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
14	5 13	raleqbidv	$$⊢g=G\to \left(\forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\leftrightarrow \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
15	6 14	anbi12d	$$⊢g=G\to \left(\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\leftrightarrow \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
16	15	iotabidv	$$⊢g=G\to \left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
17		df-0g	$$⊢0_{𝑔}=\left(g\in \mathrm{V}⟼\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\right)$$
18		iotaex	$$⊢\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)\in \mathrm{V}$$
19	16 17 18	fvmpt	$$⊢G\in \mathrm{V}\to 0_G=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
20		fvprc	$$⊢\neg G\in \mathrm{V}\to 0_G=\varnothing$$
21		euex	$$⊢\exists !e\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to \exists e\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
22		n0i	$$⊢e\in B\to \neg B=\varnothing$$
23		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
24	1 23	eqtrid	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
25	22 24	nsyl2	$$⊢e\in B\to G\in \mathrm{V}$$
26	25	adantr	$$⊢\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to G\in \mathrm{V}$$
27	26	exlimiv	$$⊢\exists e\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to G\in \mathrm{V}$$
28	21 27	syl	$$⊢\exists !e\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to G\in \mathrm{V}$$
29		iotanul	$$⊢\neg \exists !e\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\to \left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)=\varnothing$$
30	28 29	nsyl5	$$⊢\neg G\in \mathrm{V}\to \left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)=\varnothing$$
31	20 30	eqtr4d	$$⊢\neg G\in \mathrm{V}\to 0_G=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
32	19 31	pm2.61i	$$⊢0_G=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
33	3 32	eqtri	$$⊢\underset{\dot{}}{0}=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$