Theorem srglz

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

	Ref	Expression
Hypotheses	srgz.b	$$⊢B={\mathrm{Base}}_R$$
	srgz.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgz.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	srglz	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		srgz.b	$$⊢B={\mathrm{Base}}_R$$
2		srgz.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		srgz.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5		eqid	$$⊢{+}_R={+}_R$$
6	1 4 5 2 3	issrg	$$⊢R\in \mathrm{SRing}\leftrightarrow \left(R\in \mathrm{CMnd}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in B\left(\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y{+}_{R}z\right)=\left(x\underset{\dot{}}{·}y\right){+}_R\left(x\underset{\dot{}}{·}z\right)\wedge \left(x{+}_{R}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right){+}_R\left(y\underset{\dot{}}{·}z\right)\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\right)\right)$$
7	6	simp3bi	$$⊢R\in \mathrm{SRing}\to \forall x\in B\left(\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y{+}_{R}z\right)=\left(x\underset{\dot{}}{·}y\right){+}_R\left(x\underset{\dot{}}{·}z\right)\wedge \left(x{+}_{R}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right){+}_R\left(y\underset{\dot{}}{·}z\right)\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\right)$$
8	7	r19.21bi	$$⊢\left(R\in \mathrm{SRing}\wedge x\in B\right)\to \left(\forall y\in B\forall z\in B\left(x\underset{\dot{}}{·}\left(y{+}_{R}z\right)=\left(x\underset{\dot{}}{·}y\right){+}_R\left(x\underset{\dot{}}{·}z\right)\wedge \left(x{+}_{R}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right){+}_R\left(y\underset{\dot{}}{·}z\right)\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\wedge x\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)\right)$$
9	8	simprld	$$⊢\left(R\in \mathrm{SRing}\wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}$$
10	9	ralrimiva	$$⊢R\in \mathrm{SRing}\to \forall x\in B\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}$$
11		oveq2	$$⊢x=X\to \underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\underset{\dot{}}{·}X$$
12	11	eqeq1d	$$⊢x=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
13	12	rspcv	$$⊢X\in B\to \left(\forall x\in B\underset{\dot{}}{0}\underset{\dot{}}{·}x=\underset{\dot{}}{0}\to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
14	10 13	mpan9	$$⊢\left(R\in \mathrm{SRing}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$