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

Metamath Proof Explorer

Theorem srglz

Description: The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019)

Ref Expression
Hypotheses srgz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srgz.t ⊢ · = ( .r ‘ 𝑅 )
srgz.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion srglz ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )

Proof

Step Hyp Ref Expression
1 srgz.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srgz.t ⊢ · = ( .r ‘ 𝑅 )
3 srgz.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 1 4 5 2 3 issrg ⊢ ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) ) )
7 6 simp3bi ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
8 7 r19.21bi ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 0 · 𝑥 ) = 0 ∧ ( 𝑥 · 0 ) = 0 ) ) )
9 8 simprld ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ) → ( 0 · 𝑥 ) = 0 )
10 9 ralrimiva ⊢ ( 𝑅 ∈ SRing → ∀ 𝑥 ∈ 𝐵 ( 0 · 𝑥 ) = 0 )
11 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 0 · 𝑥 ) = ( 0 · 𝑋 ) )
12 11 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 0 · 𝑥 ) = 0 ↔ ( 0 · 𝑋 ) = 0 ) )
13 12 rspcv ⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 0 · 𝑥 ) = 0 → ( 0 · 𝑋 ) = 0 ) )
14 10 13 mpan9 ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )