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 )