Metamath Proof Explorer


Theorem rngolidm

Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010) (New usage is discouraged.)

Ref Expression
Hypotheses uridm.1
|- H = ( 2nd ` R )
uridm.2
|- X = ran ( 1st ` R )
uridm.3
|- U = ( GId ` H )
Assertion rngolidm
|- ( ( R e. RingOps /\ A e. X ) -> ( U H A ) = A )

Proof

Step Hyp Ref Expression
1 uridm.1
 |-  H = ( 2nd ` R )
2 uridm.2
 |-  X = ran ( 1st ` R )
3 uridm.3
 |-  U = ( GId ` H )
4 1 2 3 rngoidmlem
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) )
5 4 simpld
 |-  ( ( R e. RingOps /\ A e. X ) -> ( U H A ) = A )