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
⊢ B = Base R
srgidm.t
⊢ · ˙ = ⋅ R
srgidm.u
⊢ 1 ˙ = 1 R
Assertion
srglidm
⊢ R ∈ SRing ∧ X ∈ B → 1 ˙ · ˙ X = X
Proof
Step
Hyp
Ref
Expression
1
srgidm.b
⊢ B = Base R
2
srgidm.t
⊢ · ˙ = ⋅ R
3
srgidm.u
⊢ 1 ˙ = 1 R
4
1 2 3
srgidmlem
⊢ R ∈ SRing ∧ X ∈ B → 1 ˙ · ˙ X = X ∧ X · ˙ 1 ˙ = X
5
4
simpld
⊢ R ∈ SRing ∧ X ∈ B → 1 ˙ · ˙ X = X