This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{R}$
		srgidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		srgidm.u	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	issrgid	$⊢ R \in SRing \to ((I \in B \land \forall x \in B (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \leftrightarrow \underset{˙}{1} = I)$

Proof

Step	Hyp	Ref	Expression
1		srgidm.b	$⊢ B = {Base}_{R}$
2		srgidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		srgidm.u	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
6	4 3	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
7	4 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
8	1 2	srgideu	$⊢ R \in SRing \to \exists! y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
9		reurex	$⊢ \exists! y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x) \to \exists y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
10	8 9	syl	$⊢ R \in SRing \to \exists y \in B \forall x \in B (y \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} y = x)$
11	5 6 7 10	ismgmid	$⊢ R \in SRing \to ((I \in B \land \forall x \in B (I \underset{˙}{\cdot} x = x \land x \underset{˙}{\cdot} I = x)) \leftrightarrow \underset{˙}{1} = I)$