Metamath Proof Explorer
Description: The unit of a ring is an identity element for the multiplication.
(Contributed by FL, 18Apr2010) (New usage is discouraged.)


Ref 
Expression 

Hypotheses 
uridm.1 
⊢ 𝐻 = ( 2^{nd} ‘ 𝑅 ) 


uridm.2 
⊢ 𝑋 = ran ( 1^{st} ‘ 𝑅 ) 


uridm.3 
⊢ 𝑈 = ( GId ‘ 𝐻 ) 

Assertion 
rngolidm 
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐴 ) = 𝐴 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

uridm.1 
⊢ 𝐻 = ( 2^{nd} ‘ 𝑅 ) 
2 

uridm.2 
⊢ 𝑋 = ran ( 1^{st} ‘ 𝑅 ) 
3 

uridm.3 
⊢ 𝑈 = ( GId ‘ 𝐻 ) 
4 
1 2 3

rngoidmlem 
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐻 𝑈 ) = 𝐴 ) ) 
5 
4

simpld 
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐴 ) = 𝐴 ) 