Theorem dfur2

Description: The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	dfur2.b	$$⊢B={\mathrm{Base}}_R$$
	dfur2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	dfur2.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	dfur2	$$⊢\underset{\dot{}}{1}=\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		dfur2.b	$$⊢B={\mathrm{Base}}_R$$
2		dfur2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		dfur2.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	4 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
6	4 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
7	4 3	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
8	5 6 7	grpidval	$$⊢\underset{\dot{}}{1}=\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)$$