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

Metamath Proof Explorer

Theorem unitnegcl

Description: The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses unitnegcl.1 
|- U = ( Unit ` R )
unitnegcl.2 
|- N = ( invg ` R )
Assertion unitnegcl 
|- ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )

Proof

Step Hyp Ref Expression
1 unitnegcl.1 
 |-  U = ( Unit ` R )
2 unitnegcl.2 
 |-  N = ( invg ` R )
3 simpl 
 |-  ( ( R e. Ring /\ X e. U ) -> R e. Ring )
4 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 1 unitcl 
 |-  ( X e. U -> X e. ( Base ` R ) )
7 5 2 grpinvcl 
 |-  ( ( R e. Grp /\ X e. ( Base ` R ) ) -> ( N ` X ) e. ( Base ` R ) )
8 4 6 7 syl2an 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. ( Base ` R ) )
9 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
10 5 9 2 dvdsrneg 
 |-  ( ( R e. Ring /\ ( N ` X ) e. ( Base ` R ) ) -> ( N ` X ) ( ||r ` R ) ( N ` ( N ` X ) ) )
11 8 10 syldan 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` R ) ( N ` ( N ` X ) ) )
12 5 2 grpinvinv 
 |-  ( ( R e. Grp /\ X e. ( Base ` R ) ) -> ( N ` ( N ` X ) ) = X )
13 4 6 12 syl2an 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` ( N ` X ) ) = X )
14 11 13 breqtrd 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` R ) X )
15 simpr 
 |-  ( ( R e. Ring /\ X e. U ) -> X e. U )
16 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
17 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
18 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
19 1 16 9 17 18 isunit 
 |-  ( X e. U <-> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
20 15 19 sylib 
 |-  ( ( R e. Ring /\ X e. U ) -> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
21 20 simpld 
 |-  ( ( R e. Ring /\ X e. U ) -> X ( ||r ` R ) ( 1r ` R ) )
22 5 9 dvdsrtr 
 |-  ( ( R e. Ring /\ ( N ` X ) ( ||r ` R ) X /\ X ( ||r ` R ) ( 1r ` R ) ) -> ( N ` X ) ( ||r ` R ) ( 1r ` R ) )
23 3 14 21 22 syl3anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` R ) ( 1r ` R ) )
24 17 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
25 24 adantr 
 |-  ( ( R e. Ring /\ X e. U ) -> ( oppR ` R ) e. Ring )
26 17 5 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
27 17 2 opprneg 
 |-  N = ( invg ` ( oppR ` R ) )
28 26 18 27 dvdsrneg 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( N ` X ) e. ( Base ` R ) ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( N ` ( N ` X ) ) )
29 25 8 28 syl2anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( N ` ( N ` X ) ) )
30 29 13 breqtrd 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) X )
31 20 simprd 
 |-  ( ( R e. Ring /\ X e. U ) -> X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
32 26 18 dvdsrtr 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( N ` X ) ( ||r ` ( oppR ` R ) ) X /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
33 25 30 31 32 syl3anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
34 1 16 9 17 18 isunit 
 |-  ( ( N ` X ) e. U <-> ( ( N ` X ) ( ||r ` R ) ( 1r ` R ) /\ ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
35 23 33 34 sylanbrc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )