# Metamath Proof Explorer

## 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 ) )`