Metamath Proof Explorer


Theorem srgrz

Description: The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgz.b B = Base R
srgz.t · ˙ = R
srgz.z 0 ˙ = 0 R
Assertion srgrz R SRing X B X · ˙ 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 srgz.b B = Base R
2 srgz.t · ˙ = R
3 srgz.z 0 ˙ = 0 R
4 eqid mulGrp R = mulGrp R
5 eqid + R = + R
6 1 4 5 2 3 issrg R SRing R CMnd mulGrp R Mnd x B y B z B x · ˙ y + R z = x · ˙ y + R x · ˙ z x + R y · ˙ z = x · ˙ z + R y · ˙ z 0 ˙ · ˙ x = 0 ˙ x · ˙ 0 ˙ = 0 ˙
7 6 simp3bi R SRing x B y B z B x · ˙ y + R z = x · ˙ y + R x · ˙ z x + R y · ˙ z = x · ˙ z + R y · ˙ z 0 ˙ · ˙ x = 0 ˙ x · ˙ 0 ˙ = 0 ˙
8 7 r19.21bi R SRing x B y B z B x · ˙ y + R z = x · ˙ y + R x · ˙ z x + R y · ˙ z = x · ˙ z + R y · ˙ z 0 ˙ · ˙ x = 0 ˙ x · ˙ 0 ˙ = 0 ˙
9 8 simprrd R SRing x B x · ˙ 0 ˙ = 0 ˙
10 9 ralrimiva R SRing x B x · ˙ 0 ˙ = 0 ˙
11 oveq1 x = X x · ˙ 0 ˙ = X · ˙ 0 ˙
12 11 eqeq1d x = X x · ˙ 0 ˙ = 0 ˙ X · ˙ 0 ˙ = 0 ˙
13 12 rspcv X B x B x · ˙ 0 ˙ = 0 ˙ X · ˙ 0 ˙ = 0 ˙
14 10 13 mpan9 R SRing X B X · ˙ 0 ˙ = 0 ˙