# Metamath Proof Explorer

## Theorem rngosubdi

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 rngosubdi ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}\left({B}{D}{C}\right)=\left({A}{H}{B}\right){D}\left({A}{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 {B}\in {X}\wedge {C}\in {X}\right)\to {B}{D}{C}={B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)$
7 6 3adant3r1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{D}{C}={B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)$
8 7 oveq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}\left({B}{D}{C}\right)={A}{H}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
9 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{H}{B}\in {X}$
10 9 3adant3r3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}{B}\in {X}$
11 1 2 3 rngocl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{H}{C}\in {X}$
12 11 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}$
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}{B}\in {X}\wedge {A}{H}{C}\in {X}\right)$
14 1 3 5 4 rngosub ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}{H}{B}\in {X}\wedge {A}{H}{C}\in {X}\right)\to \left({A}{H}{B}\right){D}\left({A}{H}{C}\right)=\left({A}{H}{B}\right){G}\mathrm{inv}\left({G}\right)\left({A}{H}{C}\right)$
15 14 3expb ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}{H}{B}\in {X}\wedge {A}{H}{C}\in {X}\right)\right)\to \left({A}{H}{B}\right){D}\left({A}{H}{C}\right)=\left({A}{H}{B}\right){G}\mathrm{inv}\left({G}\right)\left({A}{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}{B}\right){D}\left({A}{H}{C}\right)=\left({A}{H}{B}\right){G}\mathrm{inv}\left({G}\right)\left({A}{H}{C}\right)$
17 idd ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to {A}\in {X}\right)$
18 idd ${⊢}{R}\in \mathrm{RingOps}\to \left({B}\in {X}\to {B}\in {X}\right)$
19 1 3 5 rngonegcl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {C}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}$
20 19 ex ${⊢}{R}\in \mathrm{RingOps}\to \left({C}\in {X}\to \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}\right)$
21 17 18 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 {B}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({C}\right)\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 {B}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}\right)$
23 1 2 3 rngodi ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}\right)\right)\to {A}{H}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)=\left({A}{H}{B}\right){G}\left({A}{H}\mathrm{inv}\left({G}\right)\left({C}\right)\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 {A}{H}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)=\left({A}{H}{B}\right){G}\left({A}{H}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
25 1 2 3 5 rngonegrmul ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({A}{H}{C}\right)={A}{H}\mathrm{inv}\left({G}\right)\left({C}\right)$
26 25 3adant3r2 ${⊢}\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({A}{H}{C}\right)={A}{H}\mathrm{inv}\left({G}\right)\left({C}\right)$
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}{B}\right){G}\mathrm{inv}\left({G}\right)\left({A}{H}{C}\right)=\left({A}{H}{B}\right){G}\left({A}{H}\mathrm{inv}\left({G}\right)\left({C}\right)\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 {A}{H}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)=\left({A}{H}{B}\right){G}\mathrm{inv}\left({G}\right)\left({A}{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}{B}\right){D}\left({A}{H}{C}\right)={A}{H}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
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 {A}{H}\left({B}{D}{C}\right)=\left({A}{H}{B}\right){D}\left({A}{H}{C}\right)$