# 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 ) )`