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

Metamath Proof Explorer

Theorem ringlidmd

Description: The unity element of a ring is a left multiplicative identity. (Contributed by SN, 14-Aug-2024)

Ref Expression
Hypotheses ringlidmd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringlidmd.t ⊢ · = ( .r ‘ 𝑅 )
ringlidmd.u ⊢ 1 = ( 1r ‘ 𝑅 )
ringlidmd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringlidmd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ringlidmd ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ringlidmd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringlidmd.t ⊢ · = ( .r ‘ 𝑅 )
3 ringlidmd.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 ringlidmd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ringlidmd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 1 2 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )
7 4 5 6 syl2anc ⊢ ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )