Theorem rngoid

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	|- G = ( 1st ` R )
	ringi.2	|- H = ( 2nd ` R )
	ringi.3	|- X = ran G
Assertion	rngoid	|- ( ( R e. RingOps /\ A e. X ) -> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	|- G = ( 1st ` R )
2		ringi.2	|- H = ( 2nd ` R )
3		ringi.3	|- X = ran G
4	1 2 3	rngoi	|- ( R e. RingOps -> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. u e. X A. x e. X A. y e. X ( ( ( u H x ) H y ) = ( u H ( x H y ) ) /\ ( u H ( x G y ) ) = ( ( u H x ) G ( u H y ) ) /\ ( ( u G x ) H y ) = ( ( u H y ) G ( x H y ) ) ) /\ E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) ) ) )
5	4	simprrd	|- ( R e. RingOps -> E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) )
6		r19.12	|- ( E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) -> A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) )
7	5 6	syl	|- ( R e. RingOps -> A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) )
8		oveq2	|- ( x = A -> ( u H x ) = ( u H A ) )
9		id	|- ( x = A -> x = A )
10	8 9	eqeq12d	|- ( x = A -> ( ( u H x ) = x <-> ( u H A ) = A ) )
11		oveq1	|- ( x = A -> ( x H u ) = ( A H u ) )
12	11 9	eqeq12d	|- ( x = A -> ( ( x H u ) = x <-> ( A H u ) = A ) )
13	10 12	anbi12d	|- ( x = A -> ( ( ( u H x ) = x /\ ( x H u ) = x ) <-> ( ( u H A ) = A /\ ( A H u ) = A ) ) )
14	13	rexbidv	|- ( x = A -> ( E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) <-> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) ) )
15	14	rspccva	|- ( ( A. x e. X E. u e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A e. X ) -> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) )
16	7 15	sylan	|- ( ( R e. RingOps /\ A e. X ) -> E. u e. X ( ( u H A ) = A /\ ( A H u ) = A ) )