Theorem srglidm

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 · 𝑋 ) = 𝑋 )