Metamath Proof Explorer


Theorem srgideu

Description: The unit element of a semiring is unique. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgcl.b B = Base R
srgcl.t · ˙ = R
Assertion srgideu R SRing ∃! u B x B u · ˙ x = x x · ˙ u = x

Proof

Step Hyp Ref Expression
1 srgcl.b B = Base R
2 srgcl.t · ˙ = R
3 eqid mulGrp R = mulGrp R
4 3 srgmgp R SRing mulGrp R Mnd
5 3 1 mgpbas B = Base mulGrp R
6 3 2 mgpplusg · ˙ = + mulGrp R
7 5 6 mndideu mulGrp R Mnd ∃! u B x B u · ˙ x = x x · ˙ u = x
8 4 7 syl R SRing ∃! u B x B u · ˙ x = x x · ˙ u = x