# Metamath Proof Explorer

## Theorem rngonegmn1r

Description: Negation in a ring is the same as right multiplication by -u 1 . (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ringneg.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringneg.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
ringneg.3 ${⊢}{X}=\mathrm{ran}{G}$
ringneg.4 ${⊢}{N}=\mathrm{inv}\left({G}\right)$
ringneg.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion rngonegmn1r ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {N}\left({A}\right)={A}{H}{N}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 ringneg.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringneg.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ringneg.3 ${⊢}{X}=\mathrm{ran}{G}$
4 ringneg.4 ${⊢}{N}=\mathrm{inv}\left({G}\right)$
5 ringneg.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
6 1 rneqi ${⊢}\mathrm{ran}{G}=\mathrm{ran}{1}^{st}\left({R}\right)$
7 3 6 eqtri ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
8 7 2 5 rngo1cl ${⊢}{R}\in \mathrm{RingOps}\to {U}\in {X}$
9 1 3 4 rngonegcl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\in {X}\right)\to {N}\left({U}\right)\in {X}$
10 8 9 mpdan ${⊢}{R}\in \mathrm{RingOps}\to {N}\left({U}\right)\in {X}$
11 10 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {N}\left({U}\right)\in {X}$
12 8 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {U}\in {X}$
13 11 12 jca ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({N}\left({U}\right)\in {X}\wedge {U}\in {X}\right)$
14 1 2 3 rngodi ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {N}\left({U}\right)\in {X}\wedge {U}\in {X}\right)\right)\to {A}{H}\left({N}\left({U}\right){G}{U}\right)=\left({A}{H}{N}\left({U}\right)\right){G}\left({A}{H}{U}\right)$
15 14 3exp2 ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to \left({N}\left({U}\right)\in {X}\to \left({U}\in {X}\to {A}{H}\left({N}\left({U}\right){G}{U}\right)=\left({A}{H}{N}\left({U}\right)\right){G}\left({A}{H}{U}\right)\right)\right)\right)$
16 15 imp43 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge \left({N}\left({U}\right)\in {X}\wedge {U}\in {X}\right)\right)\to {A}{H}\left({N}\left({U}\right){G}{U}\right)=\left({A}{H}{N}\left({U}\right)\right){G}\left({A}{H}{U}\right)$
17 13 16 mpdan ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}\left({N}\left({U}\right){G}{U}\right)=\left({A}{H}{N}\left({U}\right)\right){G}\left({A}{H}{U}\right)$
18 eqid ${⊢}\mathrm{GId}\left({G}\right)=\mathrm{GId}\left({G}\right)$
19 1 3 4 18 rngoaddneg2 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\in {X}\right)\to {N}\left({U}\right){G}{U}=\mathrm{GId}\left({G}\right)$
20 8 19 mpdan ${⊢}{R}\in \mathrm{RingOps}\to {N}\left({U}\right){G}{U}=\mathrm{GId}\left({G}\right)$
21 20 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {N}\left({U}\right){G}{U}=\mathrm{GId}\left({G}\right)$
22 21 oveq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}\left({N}\left({U}\right){G}{U}\right)={A}{H}\mathrm{GId}\left({G}\right)$
23 18 3 1 2 rngorz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}\mathrm{GId}\left({G}\right)=\mathrm{GId}\left({G}\right)$
24 22 23 eqtrd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}\left({N}\left({U}\right){G}{U}\right)=\mathrm{GId}\left({G}\right)$
25 2 7 5 rngoridm ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}{U}={A}$
26 25 oveq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({A}{H}{N}\left({U}\right)\right){G}\left({A}{H}{U}\right)=\left({A}{H}{N}\left({U}\right)\right){G}{A}$
27 17 24 26 3eqtr3rd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({A}{H}{N}\left({U}\right)\right){G}{A}=\mathrm{GId}\left({G}\right)$
28 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {N}\left({U}\right)\in {X}\right)\to {A}{H}{N}\left({U}\right)\in {X}$
29 11 28 mpd3an3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {A}{H}{N}\left({U}\right)\in {X}$
30 1 rngogrpo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{GrpOp}$
31 3 18 4 grpoinvid2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {A}{H}{N}\left({U}\right)\in {X}\right)\to \left({N}\left({A}\right)={A}{H}{N}\left({U}\right)↔\left({A}{H}{N}\left({U}\right)\right){G}{A}=\mathrm{GId}\left({G}\right)\right)$
32 30 31 syl3an1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {A}{H}{N}\left({U}\right)\in {X}\right)\to \left({N}\left({A}\right)={A}{H}{N}\left({U}\right)↔\left({A}{H}{N}\left({U}\right)\right){G}{A}=\mathrm{GId}\left({G}\right)\right)$
33 29 32 mpd3an3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left({N}\left({A}\right)={A}{H}{N}\left({U}\right)↔\left({A}{H}{N}\left({U}\right)\right){G}{A}=\mathrm{GId}\left({G}\right)\right)$
34 27 33 mpbird ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {N}\left({A}\right)={A}{H}{N}\left({U}\right)$