# 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}={\mathrm{Base}}_{{R}}$
ringnegl.t
ringnegl.u
ringnegl.n ${⊢}{N}={inv}_{g}\left({R}\right)$
ringnegl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
ringnegl.x ${⊢}{\phi }\to {X}\in {B}$
Assertion ringnegl

### Proof

Step Hyp Ref Expression
1 ringnegl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 ringnegl.t
3 ringnegl.u
4 ringnegl.n ${⊢}{N}={inv}_{g}\left({R}\right)$
5 ringnegl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
6 ringnegl.x ${⊢}{\phi }\to {X}\in {B}$
7 1 3 ringidcl
8 5 7 syl
9 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
10 5 9 syl ${⊢}{\phi }\to {R}\in \mathrm{Grp}$
11 1 4 grpinvcl
12 10 8 11 syl2anc
13 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
14 1 13 2 ringdir
15 5 8 12 6 14 syl13anc
16 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
17 1 13 16 4 grprinv
18 10 8 17 syl2anc
19 18 oveq1d
20 1 2 16 ringlz
21 5 6 20 syl2anc
22 19 21 eqtrd
23 1 2 3 ringlidm
24 5 6 23 syl2anc
25 24 oveq1d
26 15 22 25 3eqtr3rd
27 1 2 ringcl
28 5 12 6 27 syl3anc
29 1 13 16 4 grpinvid1
30 10 6 28 29 syl3anc
31 26 30 mpbird
32 31 eqcomd