Theorem ringadd2

Description: A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 24-Aug-2021)

	Ref	Expression
Hypotheses	ringadd2.b	$$⊢B={\mathrm{Base}}_R$$
	ringadd2.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	ringadd2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	ringadd2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \exists x\in BX\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		ringadd2.b	$$⊢B={\mathrm{Base}}_R$$
2		ringadd2.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ringadd2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4	1 3	ringid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \exists x\in B\left(x\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}x=X\right)$$
5		oveq12	$$⊢\left(x\underset{\dot{}}{·}X=X\wedge x\underset{\dot{}}{·}X=X\right)\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)=X\underset{\dot{}}{+}X$$
6	5	anidms	$$⊢x\underset{\dot{}}{·}X=X\to \left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)=X\underset{\dot{}}{+}X$$
7	6	eqcomd	$$⊢x\underset{\dot{}}{·}X=X\to X\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)$$
8		simpll	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to R\in \mathrm{Ring}$$
9		simpr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to x\in B$$
10		simplr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to X\in B$$
11	1 2 3	ringdir	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in B\wedge x\in B\wedge X\in B\right)\right)\to \left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X=\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)$$
12	8 9 9 10 11	syl13anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to \left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X=\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)$$
13	12	eqeq2d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to \left(X\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X\leftrightarrow X\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}X\right)\right)$$
14	7 13	syl5ibr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to \left(x\underset{\dot{}}{·}X=X\to X\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X\right)$$
15	14	adantrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to \left(\left(x\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}x=X\right)\to X\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X\right)$$
16	15	reximdva	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\exists x\in B\left(x\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}x=X\right)\to \exists x\in BX\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X\right)$$
17	4 16	mpd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \exists x\in BX\underset{\dot{}}{+}X=\left(x\underset{\dot{}}{+}x\right)\underset{\dot{}}{·}X$$