Theorem ringidval

Description: The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ringidval.g	$$⊢G={\mathrm{mulGrp}}_R$$
	ringidval.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringidval	$$⊢\underset{\dot{}}{1}=0_G$$

Proof

Step	Hyp	Ref	Expression
1		ringidval.g	$$⊢G={\mathrm{mulGrp}}_R$$
2		ringidval.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		df-ur	$$⊢1_r=0_{𝑔}\circ \mathrm{mulGrp}$$
4	3	fveq1i	$$⊢1_R=\left(0_{𝑔}\circ \mathrm{mulGrp}\right)\left(R\right)$$
5		fnmgp	$$⊢\mathrm{mulGrp}Fn\mathrm{V}$$
6		fvco2	$$⊢\left(\mathrm{mulGrp}Fn\mathrm{V}\wedge R\in \mathrm{V}\right)\to \left(0_{𝑔}\circ \mathrm{mulGrp}\right)\left(R\right)=0_{{\mathrm{mulGrp}}_R}$$
7	5 6	mpan	$$⊢R\in \mathrm{V}\to \left(0_{𝑔}\circ \mathrm{mulGrp}\right)\left(R\right)=0_{{\mathrm{mulGrp}}_R}$$
8	4 7	syl5eq	$$⊢R\in \mathrm{V}\to 1_R=0_{{\mathrm{mulGrp}}_R}$$
9		0g0	$$⊢\varnothing =0_{\varnothing }$$
10		fvprc	$$⊢\neg R\in \mathrm{V}\to 1_R=\varnothing$$
11		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{mulGrp}}_R=\varnothing$$
12	11	fveq2d	$$⊢\neg R\in \mathrm{V}\to 0_{{\mathrm{mulGrp}}_R}=0_{\varnothing }$$
13	9 10 12	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to 1_R=0_{{\mathrm{mulGrp}}_R}$$
14	8 13	pm2.61i	$$⊢1_R=0_{{\mathrm{mulGrp}}_R}$$
15	1	fveq2i	$$⊢0_G=0_{{\mathrm{mulGrp}}_R}$$
16	14 2 15	3eqtr4i	$$⊢\underset{\dot{}}{1}=0_G$$