Theorem isringid

Description: Properties showing that an element I is the unity element of a ring. (Contributed by NM, 7-Aug-2013)

	Ref	Expression
Hypotheses	rngidm.b	|- B = ( Base ` R )
	rngidm.t	|- .x. = ( .r ` R )
	rngidm.u	|- .1. = ( 1r ` R )
Assertion	isringid	|- ( R e. Ring -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )

Proof

Step	Hyp	Ref	Expression
1		rngidm.b	|- B = ( Base ` R )
2		rngidm.t	|- .x. = ( .r ` R )
3		rngidm.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	ringideu	|- ( R e. Ring -> 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. Ring -> E. y e. B A. x e. B ( ( y .x. x ) = x /\ ( x .x. y ) = x ) )
11	5 6 7 10	ismgmid	|- ( R e. Ring -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )