# Metamath Proof Explorer

## Theorem rngoneglmul

Description: Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010)

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

### Proof

Step Hyp Ref Expression
1 ringnegmul.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringnegmul.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ringnegmul.3 ${⊢}{X}=\mathrm{ran}{G}$
4 ringnegmul.4 ${⊢}{N}=\mathrm{inv}\left({G}\right)$
5 1 rneqi ${⊢}\mathrm{ran}{G}=\mathrm{ran}{1}^{st}\left({R}\right)$
6 3 5 eqtri ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
7 eqid ${⊢}\mathrm{GId}\left({H}\right)=\mathrm{GId}\left({H}\right)$
8 6 2 7 rngo1cl ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{GId}\left({H}\right)\in {X}$
9 1 3 4 rngonegcl ${⊢}\left({R}\in \mathrm{RingOps}\wedge \mathrm{GId}\left({H}\right)\in {X}\right)\to {N}\left(\mathrm{GId}\left({H}\right)\right)\in {X}$
10 8 9 mpdan ${⊢}{R}\in \mathrm{RingOps}\to {N}\left(\mathrm{GId}\left({H}\right)\right)\in {X}$
11 1 2 3 rngoass ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({N}\left(\mathrm{GId}\left({H}\right)\right)\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}\right){H}{B}={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)$
12 11 3exp2 ${⊢}{R}\in \mathrm{RingOps}\to \left({N}\left(\mathrm{GId}\left({H}\right)\right)\in {X}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}\right){H}{B}={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)\right)\right)\right)$
13 10 12 mpd ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}\right){H}{B}={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)\right)\right)$
14 13 3imp ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}\right){H}{B}={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)$
15 1 2 3 4 7 rngonegmn1l ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to {N}\left({A}\right)={N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}$
16 15 3adant3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}\right)={N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}$
17 16 oveq1d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}\right){H}{B}=\left({N}\left(\mathrm{GId}\left({H}\right)\right){H}{A}\right){H}{B}$
18 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{H}{B}\in {X}$
19 18 3expb ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{H}{B}\in {X}$
20 1 2 3 4 7 rngonegmn1l ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}{H}{B}\in {X}\right)\to {N}\left({A}{H}{B}\right)={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)$
21 19 20 syldan ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {N}\left({A}{H}{B}\right)={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)$
22 21 3impb ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{H}{B}\right)={N}\left(\mathrm{GId}\left({H}\right)\right){H}\left({A}{H}{B}\right)$
23 14 17 22 3eqtr4rd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {N}\left({A}{H}{B}\right)={N}\left({A}\right){H}{B}$