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

Metamath Proof Explorer

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 = {Base}_{R}$
		srgz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		srgz.z	$⊢ \underset{˙}{0} = 0_{R}$
		srgisid.1	$⊢ φ \to R \in SRing$
		srgisid.2	$⊢ φ \to Z \in B$
		srgisid.3	$⊢ (φ \land x \in B) \to Z \underset{˙}{\cdot} x = Z$
	Assertion	srgisid	$⊢ φ \to Z = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		srgz.b	$⊢ B = {Base}_{R}$
2		srgz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		srgz.z	$⊢ \underset{˙}{0} = 0_{R}$
4		srgisid.1	$⊢ φ \to R \in SRing$
5		srgisid.2	$⊢ φ \to Z \in B$
6		srgisid.3	$⊢ (φ \land x \in B) \to Z \underset{˙}{\cdot} x = Z$
7	6	ralrimiva	$⊢ φ \to \forall x \in B Z \underset{˙}{\cdot} x = Z$
8	1 3	srg0cl	$⊢ R \in SRing \to \underset{˙}{0} \in B$
9		oveq2	$⊢ x = \underset{˙}{0} \to Z \underset{˙}{\cdot} x = Z \underset{˙}{\cdot} \underset{˙}{0}$
10	9	eqeq1d	$⊢ x = \underset{˙}{0} \to (Z \underset{˙}{\cdot} x = Z \leftrightarrow Z \underset{˙}{\cdot} \underset{˙}{0} = Z)$
11	10	rspcv	$⊢ \underset{˙}{0} \in B \to (\forall x \in B Z \underset{˙}{\cdot} x = Z \to Z \underset{˙}{\cdot} \underset{˙}{0} = Z)$
12	4 8 11	3syl	$⊢ φ \to (\forall x \in B Z \underset{˙}{\cdot} x = Z \to Z \underset{˙}{\cdot} \underset{˙}{0} = Z)$
13	7 12	mpd	$⊢ φ \to Z \underset{˙}{\cdot} \underset{˙}{0} = Z$
14	1 2 3	srgrz	$⊢ (R \in SRing \land Z \in B) \to Z \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
15	4 5 14	syl2anc	$⊢ φ \to Z \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
16	13 15	eqtr3d	$⊢ φ \to Z = \underset{˙}{0}$