Metamath Proof Explorer

Theorem ringnegr

Description: Negation in a ring is the same as right multiplication by -1. ( rngonegmn1r analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringnegl.b 
|- B = ( Base ` R )
ringnegl.t 
|- .x. = ( .r ` R )
ringnegl.u 
|- .1. = ( 1r ` R )
ringnegl.n 
|- N = ( invg ` R )
ringnegl.r 
|- ( ph -> R e. Ring )
ringnegl.x 
|- ( ph -> X e. B )
Assertion ringnegr 
|- ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 ringnegl.b 
 |-  B = ( Base ` R )
2 ringnegl.t 
 |-  .x. = ( .r ` R )
3 ringnegl.u 
 |-  .1. = ( 1r ` R )
4 ringnegl.n 
 |-  N = ( invg ` R )
5 ringnegl.r 
 |-  ( ph -> R e. Ring )
6 ringnegl.x 
 |-  ( ph -> X e. B )
7 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
8 5 7 syl 
 |-  ( ph -> R e. Grp )
9 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
10 5 9 syl 
 |-  ( ph -> .1. e. B )
11 1 4 grpinvcl 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( N ` .1. ) e. B )
12 8 10 11 syl2anc 
 |-  ( ph -> ( N ` .1. ) e. B )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 1 13 2 ringdi 
 |-  ( ( R e. Ring /\ ( X e. B /\ ( N ` .1. ) e. B /\ .1. e. B ) ) -> ( X .x. ( ( N ` .1. ) ( +g ` R ) .1. ) ) = ( ( X .x. ( N ` .1. ) ) ( +g ` R ) ( X .x. .1. ) ) )
15 5 6 12 10 14 syl13anc 
 |-  ( ph -> ( X .x. ( ( N ` .1. ) ( +g ` R ) .1. ) ) = ( ( X .x. ( N ` .1. ) ) ( +g ` R ) ( X .x. .1. ) ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 1 13 16 4 grplinv 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( ( N ` .1. ) ( +g ` R ) .1. ) = ( 0g ` R ) )
18 8 10 17 syl2anc 
 |-  ( ph -> ( ( N ` .1. ) ( +g ` R ) .1. ) = ( 0g ` R ) )
19 18 oveq2d 
 |-  ( ph -> ( X .x. ( ( N ` .1. ) ( +g ` R ) .1. ) ) = ( X .x. ( 0g ` R ) ) )
20 1 2 16 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. ( 0g ` R ) ) = ( 0g ` R ) )
21 5 6 20 syl2anc 
 |-  ( ph -> ( X .x. ( 0g ` R ) ) = ( 0g ` R ) )
22 19 21 eqtrd 
 |-  ( ph -> ( X .x. ( ( N ` .1. ) ( +g ` R ) .1. ) ) = ( 0g ` R ) )
23 1 2 3 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .1. ) = X )
24 5 6 23 syl2anc 
 |-  ( ph -> ( X .x. .1. ) = X )
25 24 oveq2d 
 |-  ( ph -> ( ( X .x. ( N ` .1. ) ) ( +g ` R ) ( X .x. .1. ) ) = ( ( X .x. ( N ` .1. ) ) ( +g ` R ) X ) )
26 15 22 25 3eqtr3rd 
 |-  ( ph -> ( ( X .x. ( N ` .1. ) ) ( +g ` R ) X ) = ( 0g ` R ) )
27 1 2 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ ( N ` .1. ) e. B ) -> ( X .x. ( N ` .1. ) ) e. B )
28 5 6 12 27 syl3anc 
 |-  ( ph -> ( X .x. ( N ` .1. ) ) e. B )
29 1 13 16 4 grpinvid2 
 |-  ( ( R e. Grp /\ X e. B /\ ( X .x. ( N ` .1. ) ) e. B ) -> ( ( N ` X ) = ( X .x. ( N ` .1. ) ) <-> ( ( X .x. ( N ` .1. ) ) ( +g ` R ) X ) = ( 0g ` R ) ) )
30 8 6 28 29 syl3anc 
 |-  ( ph -> ( ( N ` X ) = ( X .x. ( N ` .1. ) ) <-> ( ( X .x. ( N ` .1. ) ) ( +g ` R ) X ) = ( 0g ` R ) ) )
31 26 30 mpbird 
 |-  ( ph -> ( N ` X ) = ( X .x. ( N ` .1. ) ) )
32 31 eqcomd 
 |-  ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) )