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

Metamath Proof Explorer

Theorem dvdsrneg

Description: An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses dvdsr.1 
|- B = ( Base ` R )
dvdsr.2 
|- .|| = ( ||r ` R )
dvdsrneg.5 
|- N = ( invg ` R )
Assertion dvdsrneg 
|- ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )

Proof

Step Hyp Ref Expression
1 dvdsr.1 
 |-  B = ( Base ` R )
2 dvdsr.2 
 |-  .|| = ( ||r ` R )
3 dvdsrneg.5 
 |-  N = ( invg ` R )
4 id 
 |-  ( X e. B -> X e. B )
5 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 1 6 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
8 1 3 grpinvcl 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. B ) -> ( N ` ( 1r ` R ) ) e. B )
9 5 7 8 syl2anc 
 |-  ( R e. Ring -> ( N ` ( 1r ` R ) ) e. B )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 1 2 10 dvdsrmul 
 |-  ( ( X e. B /\ ( N ` ( 1r ` R ) ) e. B ) -> X .|| ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) )
12 4 9 11 syl2anr 
 |-  ( ( R e. Ring /\ X e. B ) -> X .|| ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) )
13 simpl 
 |-  ( ( R e. Ring /\ X e. B ) -> R e. Ring )
14 simpr 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. B )
15 1 10 6 3 13 14 ringnegl 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( N ` ( 1r ` R ) ) ( .r ` R ) X ) = ( N ` X ) )
16 12 15 breqtrd 
 |-  ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )