ringidval

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

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

Metamath Proof Explorer