Theorem srgisid

Description: In a semiring, the only left-absorbing element is the additive identity. Remark in Golan p. 1. (Contributed by Thierry Arnoux, 1-May-2018)

	Ref	Expression
Hypotheses	srgz.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	srgz.t	⊢ · = ( .r ‘ 𝑅 )
	srgz.z	⊢ 0 = ( 0g ‘ 𝑅 )
	srgisid.1	⊢ ( 𝜑 → 𝑅 ∈ SRing )
	srgisid.2	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	srgisid.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑍 · 𝑥 ) = 𝑍 )
Assertion	srgisid	⊢ ( 𝜑 → 𝑍 = 0 )

Proof

Step	Hyp	Ref	Expression
1		srgz.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		srgz.t	⊢ · = ( .r ‘ 𝑅 )
3		srgz.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		srgisid.1	⊢ ( 𝜑 → 𝑅 ∈ SRing )
5		srgisid.2	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
6		srgisid.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑍 · 𝑥 ) = 𝑍 )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑍 · 𝑥 ) = 𝑍 )
8	1 3	srg0cl	⊢ ( 𝑅 ∈ SRing → 0 ∈ 𝐵 )
9		oveq2	⊢ ( 𝑥 = 0 → ( 𝑍 · 𝑥 ) = ( 𝑍 · 0 ) )
10	9	eqeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑍 · 𝑥 ) = 𝑍 ↔ ( 𝑍 · 0 ) = 𝑍 ) )
11	10	rspcv	⊢ ( 0 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑍 · 𝑥 ) = 𝑍 → ( 𝑍 · 0 ) = 𝑍 ) )
12	4 8 11	3syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑍 · 𝑥 ) = 𝑍 → ( 𝑍 · 0 ) = 𝑍 ) )
13	7 12	mpd	⊢ ( 𝜑 → ( 𝑍 · 0 ) = 𝑍 )
14	1 2 3	srgrz	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 · 0 ) = 0 )
15	4 5 14	syl2anc	⊢ ( 𝜑 → ( 𝑍 · 0 ) = 0 )
16	13 15	eqtr3d	⊢ ( 𝜑 → 𝑍 = 0 )