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

Metamath Proof Explorer

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 = {Base}_{R}$
		srgz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		srgz.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	srglz	$⊢ (R \in SRing \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \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		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5		eqid	$⊢ +_{R} = +_{R}$
6	1 4 5 2 3	issrg	$⊢ R \in SRing \leftrightarrow (R \in CMnd \land {mulGrp}_{R} \in Mnd \land \forall x \in B (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
7	6	simp3bi	$⊢ R \in SRing \to \forall x \in B (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))$
8	7	r19.21bi	$⊢ (R \in SRing \land x \in B) \to (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y +_{R} z) = (x \underset{˙}{\cdot} y) +_{R} (x \underset{˙}{\cdot} z) \land (x +_{R} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) +_{R} (y \underset{˙}{\cdot} z)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))$
9	8	simprld	$⊢ (R \in SRing \land x \in B) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
10	9	ralrimiva	$⊢ R \in SRing \to \forall x \in B \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
11		oveq2	$⊢ x = X \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} X$
12	11	eqeq1d	$⊢ x = X \to (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
13	12	rspcv	$⊢ X \in B \to (\forall x \in B \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
14	10 13	mpan9	$⊢ (R \in SRing \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$