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 = ( Base ` R )
	dvdsr.2	|- .|| = ( ||r ` R )
Assertion	dvdsrid	|- ( ( R e. Ring /\ X e. B ) -> X .|| X )

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	|- B = ( Base ` R )
2		dvdsr.2	|- .|| = ( ||r ` R )
3		id	|- ( X e. B -> X e. B )
4		eqid	|- ( 1r ` R ) = ( 1r ` R )
5	1 4	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. B )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7	1 2 6	dvdsrmul	|- ( ( X e. B /\ ( 1r ` R ) e. B ) -> X .|| ( ( 1r ` R ) ( .r ` R ) X ) )
8	3 5 7	syl2anr	|- ( ( R e. Ring /\ X e. B ) -> X .|| ( ( 1r ` R ) ( .r ` R ) X ) )
9	1 6 4	ringlidm	|- ( ( R e. Ring /\ X e. B ) -> ( ( 1r ` R ) ( .r ` R ) X ) = X )
10	8 9	breqtrd	|- ( ( R e. Ring /\ X e. B ) -> X .|| X )