# Metamath Proof Explorer

## Theorem rngosub

Description: Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ringnegcl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringnegcl.2 ${⊢}{X}=\mathrm{ran}{G}$
ringnegcl.3 ${⊢}{N}=\mathrm{inv}\left({G}\right)$
ringsub.4 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion rngosub ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={A}{G}{N}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 ringnegcl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringnegcl.2 ${⊢}{X}=\mathrm{ran}{G}$
3 ringnegcl.3 ${⊢}{N}=\mathrm{inv}\left({G}\right)$
4 ringsub.4 ${⊢}{D}={/}_{g}\left({G}\right)$
5 1 rngogrpo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{GrpOp}$
6 2 3 4 grpodivval ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={A}{G}{N}\left({B}\right)$
7 5 6 syl3an1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={A}{G}{N}\left({B}\right)$