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 )