This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringlidm

Description: The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011)

Ref Expression
Hypotheses ringidm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringidm.t ⊢ · = ( .r ‘ 𝑅 )
ringidm.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion ringlidm ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ringidm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringidm.t ⊢ · = ( .r ‘ 𝑅 )
3 ringidm.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 2 3 ringidmlem ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )
5 4 simpld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )