This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )