Theorem issrgid

Description: Properties showing that an element I is the unity element of a semiring. (Contributed by NM, 7-Aug-2013) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	srgidm.b	$$⊢B={\mathrm{Base}}_R$$
	srgidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgidm.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	issrgid	$$⊢R\in \mathrm{SRing}\to \left(\left(I\in B\wedge \forall x\in B\left(I\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}I=x\right)\right)\leftrightarrow \underset{\dot{}}{1}=I\right)$$

Proof

Step	Hyp	Ref	Expression
1		srgidm.b	$$⊢B={\mathrm{Base}}_R$$
2		srgidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		srgidm.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 3	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
7	4 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
8	1 2	srgideu	$$⊢R\in \mathrm{SRing}\to \exists !y\in B\forall x\in B\left(y\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}y=x\right)$$
9		reurex	$$⊢\exists !y\in B\forall x\in B\left(y\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}y=x\right)\to \exists y\in B\forall x\in B\left(y\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}y=x\right)$$
10	8 9	syl	$$⊢R\in \mathrm{SRing}\to \exists y\in B\forall x\in B\left(y\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}y=x\right)$$
11	5 6 7 10	ismgmid	$$⊢R\in \mathrm{SRing}\to \left(\left(I\in B\wedge \forall x\in B\left(I\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}I=x\right)\right)\leftrightarrow \underset{\dot{}}{1}=I\right)$$