Theorem ringo2times

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

	Ref	Expression
Hypotheses	ringo2times.b	$$⊢B={\mathrm{Base}}_R$$
	ringo2times.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	ringo2times.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringo2times.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringo2times	$$⊢\left(R\in \mathrm{Ring}\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		ringo2times.b	$$⊢B={\mathrm{Base}}_R$$
2		ringo2times.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ringo2times.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		ringo2times.u	$$⊢\underset{\dot{}}{1}=1_R$$
5	1 2 3	ringdir	$$⊢\left(R\in \mathrm{Ring}\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{Ring}\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{Ring}\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	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
9	8	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge A\in B\right)\to \underset{\dot{}}{1}\in B$$
10	1 3 4	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
11	10	ralrimiva	$$⊢R\in \mathrm{Ring}\to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
12	11	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge A\in B\right)\to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
13		simpr	$$⊢\left(R\in \mathrm{Ring}\wedge A\in B\right)\to A\in B$$
14	7 9 12 13	o2timesd	$$⊢\left(R\in \mathrm{Ring}\wedge A\in B\right)\to A\underset{\dot{}}{+}A=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}A$$