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	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	uridm.2	⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
	uridm.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion	rngolidm	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		uridm.1	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
2		uridm.2	⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
3		uridm.3	⊢ 𝑈 = ( GId ‘ 𝐻 )
4	1 2 3	rngoidmlem	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) )
5	4	simpld	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐴 ) = 𝐴 )