Metamath Proof Explorer


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 ∧ 𝐴𝑋 ) → ( 𝐴 𝐻 𝑈 ) = 𝐴 )