Metamath Proof Explorer

Theorem rngoideu

Description: The unit element of a ring is unique. (Contributed by NM, 4-Apr-2009) (Revised by Mario Carneiro, 21-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 rngoideu 
|- ( R e. RingOps -> E! u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) )

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 simpl 
 |-  ( ( ( u H x ) = x /\ ( x H u ) = x ) -> ( u H x ) = x )
7 6 ralimi 
 |-  ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) -> A. x e. X ( u H x ) = x )
8 oveq2 
 |-  ( x = y -> ( u H x ) = ( u H y ) )
9 id 
 |-  ( x = y -> x = y )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( u H x ) = x <-> ( u H y ) = y ) )
11 10 rspcv 
 |-  ( y e. X -> ( A. x e. X ( u H x ) = x -> ( u H y ) = y ) )
12 7 11 syl5 
 |-  ( y e. X -> ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) -> ( u H y ) = y ) )
13 simpr 
 |-  ( ( ( y H x ) = x /\ ( x H y ) = x ) -> ( x H y ) = x )
14 13 ralimi 
 |-  ( A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) -> A. x e. X ( x H y ) = x )
15 oveq1 
 |-  ( x = u -> ( x H y ) = ( u H y ) )
16 id 
 |-  ( x = u -> x = u )
17 15 16 eqeq12d 
 |-  ( x = u -> ( ( x H y ) = x <-> ( u H y ) = u ) )
18 17 rspcv 
 |-  ( u e. X -> ( A. x e. X ( x H y ) = x -> ( u H y ) = u ) )
19 14 18 syl5 
 |-  ( u e. X -> ( A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) -> ( u H y ) = u ) )
20 12 19 im2anan9r 
 |-  ( ( u e. X /\ y e. X ) -> ( ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) ) -> ( ( u H y ) = y /\ ( u H y ) = u ) ) )
21 eqtr2 
 |-  ( ( ( u H y ) = y /\ ( u H y ) = u ) -> y = u )
22 21 equcomd 
 |-  ( ( ( u H y ) = y /\ ( u H y ) = u ) -> u = y )
23 20 22 syl6 
 |-  ( ( u e. X /\ y e. X ) -> ( ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) ) -> u = y ) )
24 23 rgen2 
 |-  A. u e. X A. y e. X ( ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) ) -> u = y )
25 oveq1 
 |-  ( u = y -> ( u H x ) = ( y H x ) )
26 25 eqeq1d 
 |-  ( u = y -> ( ( u H x ) = x <-> ( y H x ) = x ) )
27 26 ovanraleqv 
 |-  ( u = y -> ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) <-> A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) ) )
28 27 reu4 
 |-  ( E! u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) <-> ( E. u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A. u e. X A. y e. X ( ( A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) /\ A. x e. X ( ( y H x ) = x /\ ( x H y ) = x ) ) -> u = y ) ) )
29 5 24 28 sylanblrc 
 |-  ( R e. RingOps -> E! u e. X A. x e. X ( ( u H x ) = x /\ ( x H u ) = x ) )