Theorem o2timesd

Description: An element of a ring-like structure plus itself is two times the element. "Two" in such a structure is the sum of the unity element with itself. This (formerly) part of the proof for ringcom depends on the (right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025)

	Ref	Expression
Hypotheses	o2timesd.e	$$⊢\phi \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)$$
	o2timesd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
	o2timesd.i	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
	o2timesd.x	$$⊢\phi \to X\in B$$
Assertion	o2timesd	$$⊢\phi \to X\underset{\dot{}}{+}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		o2timesd.e	$$⊢\phi \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)$$
2		o2timesd.u	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
3		o2timesd.i	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
4		o2timesd.x	$$⊢\phi \to X\in B$$
5		oveq2	$$⊢x=X\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}\underset{\dot{}}{·}X$$
6		id	$$⊢x=X\to x=X$$
7	5 6	eqeq12d	$$⊢x=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}X=X\right)$$
8	7	rspcva	$$⊢\left(X\in B\wedge \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
9	8	eqcomd	$$⊢\left(X\in B\wedge \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\right)\to X=\underset{\dot{}}{1}\underset{\dot{}}{·}X$$
10	4 3 9	syl2anc	$$⊢\phi \to X=\underset{\dot{}}{1}\underset{\dot{}}{·}X$$
11	10 10	oveq12d	$$⊢\phi \to X\underset{\dot{}}{+}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
12	2 2 4	3jca	$$⊢\phi \to \left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\wedge X\in B\right)$$
13		oveq1	$$⊢x=\underset{\dot{}}{1}\to x\underset{\dot{}}{+}y=\underset{\dot{}}{1}\underset{\dot{}}{+}y$$
14	13	oveq1d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z$$
15		oveq1	$$⊢x=\underset{\dot{}}{1}\to x\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}z$$
16	15	oveq1d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
17	14 16	eqeq12d	$$⊢x=\underset{\dot{}}{1}\to \left(\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)$$
18		oveq2	$$⊢y=\underset{\dot{}}{1}\to \underset{\dot{}}{1}\underset{\dot{}}{+}y=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}$$
19	18	oveq1d	$$⊢y=\underset{\dot{}}{1}\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z$$
20		oveq1	$$⊢y=\underset{\dot{}}{1}\to y\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}z$$
21	20	oveq2d	$$⊢y=\underset{\dot{}}{1}\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)$$
22	19 21	eqeq12d	$$⊢y=\underset{\dot{}}{1}\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\right)$$
23		oveq2	$$⊢z=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$
24		oveq2	$$⊢z=X\to \underset{\dot{}}{1}\underset{\dot{}}{·}z=\underset{\dot{}}{1}\underset{\dot{}}{·}X$$
25	24 24	oveq12d	$$⊢z=X\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
26	23 25	eqeq12d	$$⊢z=X\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}z=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}z\right)\leftrightarrow \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)$$
27	17 22 26	rspc3v	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\wedge X\in B\right)\to \left(\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)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\right)$$
28	12 1 27	sylc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right)$$
29	11 28	eqtr4d	$$⊢\phi \to X\underset{\dot{}}{+}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$