Theorem ringid

Description: The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021)

	Ref	Expression
Hypotheses	ringid.b	|- B = ( Base ` R )
	ringid.t	|- .x. = ( .r ` R )
Assertion	ringid	|- ( ( R e. Ring /\ X e. B ) -> E. u e. B ( ( u .x. X ) = X /\ ( X .x. u ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		ringid.b	|- B = ( Base ` R )
2		ringid.t	|- .x. = ( .r ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4	1 3	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. B )
5	4	adantr	|- ( ( R e. Ring /\ X e. B ) -> ( 1r ` R ) e. B )
6		oveq1	|- ( u = ( 1r ` R ) -> ( u .x. X ) = ( ( 1r ` R ) .x. X ) )
7	6	eqeq1d	|- ( u = ( 1r ` R ) -> ( ( u .x. X ) = X <-> ( ( 1r ` R ) .x. X ) = X ) )
8		oveq2	|- ( u = ( 1r ` R ) -> ( X .x. u ) = ( X .x. ( 1r ` R ) ) )
9	8	eqeq1d	|- ( u = ( 1r ` R ) -> ( ( X .x. u ) = X <-> ( X .x. ( 1r ` R ) ) = X ) )
10	7 9	anbi12d	|- ( u = ( 1r ` R ) -> ( ( ( u .x. X ) = X /\ ( X .x. u ) = X ) <-> ( ( ( 1r ` R ) .x. X ) = X /\ ( X .x. ( 1r ` R ) ) = X ) ) )
11	10	adantl	|- ( ( ( R e. Ring /\ X e. B ) /\ u = ( 1r ` R ) ) -> ( ( ( u .x. X ) = X /\ ( X .x. u ) = X ) <-> ( ( ( 1r ` R ) .x. X ) = X /\ ( X .x. ( 1r ` R ) ) = X ) ) )
12	1 2 3	ringidmlem	|- ( ( R e. Ring /\ X e. B ) -> ( ( ( 1r ` R ) .x. X ) = X /\ ( X .x. ( 1r ` R ) ) = X ) )
13	5 11 12	rspcedvd	|- ( ( R e. Ring /\ X e. B ) -> E. u e. B ( ( u .x. X ) = X /\ ( X .x. u ) = X ) )