Theorem rngoridm

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 ‘ 𝑅 )
	uridm2.2	⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion	rngoridm	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐻 𝑈 ) = 𝐴 )

Proof

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