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 = {Base}_{R}$
	dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	dvdsrid	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} X$

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		id	$⊢ X \in B \to X \in B$
4		eqid	$⊢ 1_{R} = 1_{R}$
5	1 4	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7	1 2 6	dvdsrmul	$⊢ (X \in B \land 1_{R} \in B) \to X \underset{˙}{∥} (1_{R} \cdot_{R} X)$
8	3 5 7	syl2anr	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} (1_{R} \cdot_{R} X)$
9	1 6 4	ringlidm	$⊢ (R \in Ring \land X \in B) \to 1_{R} \cdot_{R} X = X$
10	8 9	breqtrd	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} X$

Metamath Proof Explorer