# Metamath Proof Explorer

## Theorem rngosubdir

Description: Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ringsubdi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringsubdi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
ringsubdi.3 ${⊢}{X}=\mathrm{ran}{G}$
ringsubdi.4 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion rngosubdir ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){H}{C}=\left({A}{H}{C}\right){D}\left({B}{H}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ringsubdi.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringsubdi.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 ringsubdi.3 ${⊢}{X}=\mathrm{ran}{G}$
4 ringsubdi.4 ${⊢}{D}={/}_{g}\left({G}\right)$
5 eqid ${⊢}\mathrm{inv}\left({G}\right)=\mathrm{inv}\left({G}\right)$
6 1 3 5 4 rngosub ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}={A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)$
7 6 3adant3r3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}{B}={A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)$
8 7 oveq1d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){H}{C}=\left({A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)\right){H}{C}$
9 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{H}{C}\in {X}$
10 9 3adant3r2 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}{C}\in {X}$
11 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{H}{C}\in {X}$
12 11 3adant3r1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{H}{C}\in {X}$
13 10 12 jca ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}\in {X}\wedge {B}{H}{C}\in {X}\right)$
14 1 3 5 4 rngosub ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}{H}{C}\in {X}\wedge {B}{H}{C}\in {X}\right)\to \left({A}{H}{C}\right){D}\left({B}{H}{C}\right)=\left({A}{H}{C}\right){G}\mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)$
15 14 3expb ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}{H}{C}\in {X}\wedge {B}{H}{C}\in {X}\right)\right)\to \left({A}{H}{C}\right){D}\left({B}{H}{C}\right)=\left({A}{H}{C}\right){G}\mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)$
16 13 15 syldan ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}\right){D}\left({B}{H}{C}\right)=\left({A}{H}{C}\right){G}\mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)$
17 idd ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to {A}\in {X}\right)$
18 1 3 5 rngonegcl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {B}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({B}\right)\in {X}$
19 18 ex ${⊢}{R}\in \mathrm{RingOps}\to \left({B}\in {X}\to \mathrm{inv}\left({G}\right)\left({B}\right)\in {X}\right)$
20 idd ${⊢}{R}\in \mathrm{RingOps}\to \left({C}\in {X}\to {C}\in {X}\right)$
21 17 19 20 3anim123d ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left({A}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({B}\right)\in {X}\wedge {C}\in {X}\right)\right)$
22 21 imp ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({B}\right)\in {X}\wedge {C}\in {X}\right)$
23 1 2 3 rngodir ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({B}\right)\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)\right){H}{C}=\left({A}{H}{C}\right){G}\left(\mathrm{inv}\left({G}\right)\left({B}\right){H}{C}\right)$
24 22 23 syldan ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)\right){H}{C}=\left({A}{H}{C}\right){G}\left(\mathrm{inv}\left({G}\right)\left({B}\right){H}{C}\right)$
25 1 2 3 5 rngoneglmul ${⊢}\left({R}\in \mathrm{RingOps}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)=\mathrm{inv}\left({G}\right)\left({B}\right){H}{C}$
26 25 3adant3r1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)=\mathrm{inv}\left({G}\right)\left({B}\right){H}{C}$
27 26 oveq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}\right){G}\mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)=\left({A}{H}{C}\right){G}\left(\mathrm{inv}\left({G}\right)\left({B}\right){H}{C}\right)$
28 24 27 eqtr4d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)\right){H}{C}=\left({A}{H}{C}\right){G}\mathrm{inv}\left({G}\right)\left({B}{H}{C}\right)$
29 16 28 eqtr4d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}\right){D}\left({B}{H}{C}\right)=\left({A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)\right){H}{C}$
30 8 29 eqtr4d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){H}{C}=\left({A}{H}{C}\right){D}\left({B}{H}{C}\right)$