Metamath Proof Explorer

Theorem ringnegl

Description: Negation in a ring is the same as left multiplication by -1. ( rngonegmn1l 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 ringnegl 
|- ( ph -> ( ( N ` .1. ) .x. X ) = ( 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 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
8 5 7 syl 
 |-  ( ph -> .1. e. B )
9 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
10 5 9 syl 
 |-  ( ph -> R e. Grp )
11 1 4 grpinvcl 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( N ` .1. ) e. B )
12 10 8 11 syl2anc 
 |-  ( ph -> ( N ` .1. ) e. B )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 1 13 2 ringdir 
 |-  ( ( R e. Ring /\ ( .1. e. B /\ ( N ` .1. ) e. B /\ X e. B ) ) -> ( ( .1. ( +g ` R ) ( N ` .1. ) ) .x. X ) = ( ( .1. .x. X ) ( +g ` R ) ( ( N ` .1. ) .x. X ) ) )
15 5 8 12 6 14 syl13anc 
 |-  ( ph -> ( ( .1. ( +g ` R ) ( N ` .1. ) ) .x. X ) = ( ( .1. .x. X ) ( +g ` R ) ( ( N ` .1. ) .x. X ) ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 1 13 16 4 grprinv 
 |-  ( ( R e. Grp /\ .1. e. B ) -> ( .1. ( +g ` R ) ( N ` .1. ) ) = ( 0g ` R ) )
18 10 8 17 syl2anc 
 |-  ( ph -> ( .1. ( +g ` R ) ( N ` .1. ) ) = ( 0g ` R ) )
19 18 oveq1d 
 |-  ( ph -> ( ( .1. ( +g ` R ) ( N ` .1. ) ) .x. X ) = ( ( 0g ` R ) .x. X ) )
20 1 2 16 ringlz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 0g ` R ) .x. X ) = ( 0g ` R ) )
21 5 6 20 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) .x. X ) = ( 0g ` R ) )
22 19 21 eqtrd 
 |-  ( ph -> ( ( .1. ( +g ` R ) ( N ` .1. ) ) .x. X ) = ( 0g ` R ) )
23 1 2 3 ringlidm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .1. .x. X ) = X )
24 5 6 23 syl2anc 
 |-  ( ph -> ( .1. .x. X ) = X )
25 24 oveq1d 
 |-  ( ph -> ( ( .1. .x. X ) ( +g ` R ) ( ( N ` .1. ) .x. X ) ) = ( X ( +g ` R ) ( ( N ` .1. ) .x. X ) ) )
26 15 22 25 3eqtr3rd 
 |-  ( ph -> ( X ( +g ` R ) ( ( N ` .1. ) .x. X ) ) = ( 0g ` R ) )
27 1 2 ringcl 
 |-  ( ( R e. Ring /\ ( N ` .1. ) e. B /\ X e. B ) -> ( ( N ` .1. ) .x. X ) e. B )
28 5 12 6 27 syl3anc 
 |-  ( ph -> ( ( N ` .1. ) .x. X ) e. B )
29 1 13 16 4 grpinvid1 
 |-  ( ( R e. Grp /\ X e. B /\ ( ( N ` .1. ) .x. X ) e. B ) -> ( ( N ` X ) = ( ( N ` .1. ) .x. X ) <-> ( X ( +g ` R ) ( ( N ` .1. ) .x. X ) ) = ( 0g ` R ) ) )
30 10 6 28 29 syl3anc 
 |-  ( ph -> ( ( N ` X ) = ( ( N ` .1. ) .x. X ) <-> ( X ( +g ` R ) ( ( N ` .1. ) .x. X ) ) = ( 0g ` R ) ) )
31 26 30 mpbird 
 |-  ( ph -> ( N ` X ) = ( ( N ` .1. ) .x. X ) )
32 31 eqcomd 
 |-  ( ph -> ( ( N ` .1. ) .x. X ) = ( N ` X ) )