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 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
17 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
18 1 15 9 16 17 isunit 
 |-  ( X e. U <-> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
19 18 bilani 
 |-  ( ( R e. Ring /\ X e. U ) -> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
20 19 simpld 
 |-  ( ( R e. Ring /\ X e. U ) -> X ( ||r ` R ) ( 1r ` R ) )
21 5 9 dvdsrtr 
 |-  ( ( R e. Ring /\ ( N ` X ) ( ||r ` R ) X /\ X ( ||r ` R ) ( 1r ` R ) ) -> ( N ` X ) ( ||r ` R ) ( 1r ` R ) )
22 3 14 20 21 syl3anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` R ) ( 1r ` R ) )
23 16 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
24 23 adantr 
 |-  ( ( R e. Ring /\ X e. U ) -> ( oppR ` R ) e. Ring )
25 16 5 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
26 16 2 opprneg 
 |-  N = ( invg ` ( oppR ` R ) )
27 25 17 26 dvdsrneg 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( N ` X ) e. ( Base ` R ) ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( N ` ( N ` X ) ) )
28 24 8 27 syl2anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( N ` ( N ` X ) ) )
29 28 13 breqtrd 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) X )
30 19 simprd 
 |-  ( ( R e. Ring /\ X e. U ) -> X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
31 25 17 dvdsrtr 
 |-  ( ( ( oppR ` R ) e. Ring /\ ( N ` X ) ( ||r ` ( oppR ` R ) ) X /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
32 24 29 30 31 syl3anc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
33 1 15 9 16 17 isunit 
 |-  ( ( N ` X ) e. U <-> ( ( N ` X ) ( ||r ` R ) ( 1r ` R ) /\ ( N ` X ) ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
34 22 32 33 sylanbrc 
 |-  ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )