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	$$⊢B={\mathrm{Base}}_R$$
	srgz.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgz.z	$$⊢\underset{\dot{}}{0}=0_R$$
	srgisid.1	$$⊢\phi \to R\in \mathrm{SRing}$$
	srgisid.2	$$⊢\phi \to Z\in B$$
	srgisid.3	$$⊢\left(\phi \wedge x\in B\right)\to Z\underset{\dot{}}{·}x=Z$$
Assertion	srgisid	$$⊢\phi \to Z=\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		srgisid.1	$$⊢\phi \to R\in \mathrm{SRing}$$
5		srgisid.2	$$⊢\phi \to Z\in B$$
6		srgisid.3	$$⊢\left(\phi \wedge x\in B\right)\to Z\underset{\dot{}}{·}x=Z$$
7	6	ralrimiva	$$⊢\phi \to \forall x\in BZ\underset{\dot{}}{·}x=Z$$
8	1 3	srg0cl	$$⊢R\in \mathrm{SRing}\to \underset{\dot{}}{0}\in B$$
9		oveq2	$$⊢x=\underset{\dot{}}{0}\to Z\underset{\dot{}}{·}x=Z\underset{\dot{}}{·}\underset{\dot{}}{0}$$
10	9	eqeq1d	$$⊢x=\underset{\dot{}}{0}\to \left(Z\underset{\dot{}}{·}x=Z\leftrightarrow Z\underset{\dot{}}{·}\underset{\dot{}}{0}=Z\right)$$
11	10	rspcv	$$⊢\underset{\dot{}}{0}\in B\to \left(\forall x\in BZ\underset{\dot{}}{·}x=Z\to Z\underset{\dot{}}{·}\underset{\dot{}}{0}=Z\right)$$
12	4 8 11	3syl	$$⊢\phi \to \left(\forall x\in BZ\underset{\dot{}}{·}x=Z\to Z\underset{\dot{}}{·}\underset{\dot{}}{0}=Z\right)$$
13	7 12	mpd	$$⊢\phi \to Z\underset{\dot{}}{·}\underset{\dot{}}{0}=Z$$
14	1 2 3	srgrz	$$⊢\left(R\in \mathrm{SRing}\wedge Z\in B\right)\to Z\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
15	4 5 14	syl2anc	$$⊢\phi \to Z\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	13 15	eqtr3d	$$⊢\phi \to Z=\underset{\dot{}}{0}$$