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	|- .x. = ( .r ` R )
	srgidm.u	|- .1. = ( 1r ` R )
Assertion	issrgid	|- ( R e. SRing -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )

Proof

Step	Hyp	Ref	Expression
1		srgidm.b	|- B = ( Base ` R )
2		srgidm.t	|- .x. = ( .r ` R )
3		srgidm.u	|- .1. = ( 1r ` R )
4		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
5	4 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
6	4 3	ringidval	|- .1. = ( 0g ` ( mulGrp ` R ) )
7	4 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
8	1 2	srgideu	|- ( R e. SRing -> E! y e. B A. x e. B ( ( y .x. x ) = x /\ ( x .x. y ) = x ) )
9		reurex	|- ( E! y e. B A. x e. B ( ( y .x. x ) = x /\ ( x .x. y ) = x ) -> E. y e. B A. x e. B ( ( y .x. x ) = x /\ ( x .x. y ) = x ) )
10	8 9	syl	|- ( R e. SRing -> E. y e. B A. x e. B ( ( y .x. x ) = x /\ ( x .x. y ) = x ) )
11	5 6 7 10	ismgmid	|- ( R e. SRing -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )