Database
BASIC ALGEBRAIC STRUCTURES
Rings
Semirings
srglidm
Metamath Proof Explorer
Description: The unity 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 · 𝑋 ) = 𝑋 )