Metamath Proof Explorer


Theorem srglidm

Description: The unit element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgidm.b 𝐵 = ( Base ‘ 𝑅 )
srgidm.t · = ( .r𝑅 )
srgidm.u 1 = ( 1r𝑅 )
Assertion srglidm ( ( 𝑅 ∈ SRing ∧ 𝑋𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 srgidm.b 𝐵 = ( Base ‘ 𝑅 )
2 srgidm.t · = ( .r𝑅 )
3 srgidm.u 1 = ( 1r𝑅 )
4 1 2 3 srgidmlem ( ( 𝑅 ∈ SRing ∧ 𝑋𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )
5 4 simpld ( ( 𝑅 ∈ SRing ∧ 𝑋𝐵 ) → ( 1 · 𝑋 ) = 𝑋 )