This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )