Theorem dvdsrid

Description: An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
	dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	dvdsrid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\parallel }X$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		id	$$⊢X\in B\to X\in B$$
4		eqid	$$⊢1_R=1_R$$
5	1 4	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in B$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	1 2 6	dvdsrmul	$$⊢\left(X\in B\wedge 1_R\in B\right)\to X\underset{\dot{}}{\parallel }\left(1_R{\cdot }_{R}X\right)$$
8	3 5 7	syl2anr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\parallel }\left(1_R{\cdot }_{R}X\right)$$
9	1 6 4	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to 1_R{\cdot }_{R}X=X$$
10	8 9	breqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\parallel }X$$