Metamath Proof Explorer
Description: The unit element of a ring is a right multiplicative identity.
(Contributed by NM, 15Sep2011)


Ref 
Expression 

Hypotheses 
rngidm.b 
⊢ 𝐵 = ( Base ‘ 𝑅 ) 


rngidm.t 
⊢ · = ( ._{r} ‘ 𝑅 ) 


rngidm.u 
⊢ 1 = ( 1_{r} ‘ 𝑅 ) 

Assertion 
ringridm 
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 1 ) = 𝑋 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

rngidm.b 
⊢ 𝐵 = ( Base ‘ 𝑅 ) 
2 

rngidm.t 
⊢ · = ( ._{r} ‘ 𝑅 ) 
3 

rngidm.u 
⊢ 1 = ( 1_{r} ‘ 𝑅 ) 
4 
1 2 3

ringidmlem 
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) ) 
5 
4

simprd 
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · 1 ) = 𝑋 ) 