Theorem srgo2times

Description: A semiring element plus itself is two times the element. "Two" in an arbitrary (unital) semiring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021) Variant of o2timesd for semirings. (Revised by AV, 1-Feb-2025)

	Ref	Expression
Hypotheses	srgo2times.b	$$⊢B={\mathrm{Base}}_R$$
	srgo2times.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	srgo2times.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgo2times.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	srgo2times	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to A\underset{\dot{}}{+}A=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$

Proof

Step	Hyp	Ref	Expression
1		srgo2times.b	$$⊢B={\mathrm{Base}}_R$$
2		srgo2times.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		srgo2times.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		srgo2times.u	$$⊢\underset{\dot{}}{1}=1_R$$
5	1 2 3	srgdir	$$⊢\left(R\in \mathrm{SRing}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
6	5	ralrimivvva	$$⊢R\in \mathrm{SRing}\to \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
7	6	adantr	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
8	1 4	srgidcl	$$⊢R\in \mathrm{SRing}\to \underset{\dot{}}{1}\in B$$
9	8	adantr	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to \underset{\dot{}}{1}\in B$$
10	1 3 4	srglidm	$$⊢\left(R\in \mathrm{SRing}\wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
11	10	ralrimiva	$$⊢R\in \mathrm{SRing}\to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
12	11	adantr	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
13		simpr	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to A\in B$$
14	7 9 12 13	o2timesd	$$⊢\left(R\in \mathrm{SRing}\wedge A\in B\right)\to A\underset{\dot{}}{+}A=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$