Metamath Proof Explorer

Theorem rngosubdir

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

Ref Expression
Hypotheses ringsubdi.1 ⊢G=1st⁡R
ringsubdi.2 ⊢H=2nd⁡R
ringsubdi.3 ⊢X=ran⁡G
ringsubdi.4 ⊢D=/g⁡G
Assertion rngosubdir ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→ADBHC=AHCDBHC

Proof

Step Hyp Ref Expression
1 ringsubdi.1 ⊢G=1st⁡R
2 ringsubdi.2 ⊢H=2nd⁡R
3 ringsubdi.3 ⊢X=ran⁡G
4 ringsubdi.4 ⊢D=/g⁡G
5 eqid ⊢inv⁡G=inv⁡G
6 1 3 5 4 rngosub ⊢R∈RingOps∧A∈X∧B∈X→ADB=AGinv⁡G⁡B
7 6 3adant3r3 ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→ADB=AGinv⁡G⁡B
8 7 oveq1d ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→ADBHC=AGinv⁡G⁡BHC
9 1 2 3 rngocl ⊢R∈RingOps∧A∈X∧C∈X→AHC∈X
10 9 3adant3r2 ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHC∈X
11 1 2 3 rngocl ⊢R∈RingOps∧B∈X∧C∈X→BHC∈X
12 11 3adant3r1 ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→BHC∈X
13 10 12 jca ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHC∈X∧BHC∈X
14 1 3 5 4 rngosub ⊢R∈RingOps∧AHC∈X∧BHC∈X→AHCDBHC=AHCGinv⁡G⁡BHC
15 14 3expb ⊢R∈RingOps∧AHC∈X∧BHC∈X→AHCDBHC=AHCGinv⁡G⁡BHC
16 13 15 syldan ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHCDBHC=AHCGinv⁡G⁡BHC
17 idd ⊢R∈RingOps→A∈X→A∈X
18 1 3 5 rngonegcl ⊢R∈RingOps∧B∈X→inv⁡G⁡B∈X
19 18 ex ⊢R∈RingOps→B∈X→inv⁡G⁡B∈X
20 idd ⊢R∈RingOps→C∈X→C∈X
21 17 19 20 3anim123d ⊢R∈RingOps→A∈X∧B∈X∧C∈X→A∈X∧inv⁡G⁡B∈X∧C∈X
22 21 imp ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→A∈X∧inv⁡G⁡B∈X∧C∈X
23 1 2 3 rngodir ⊢R∈RingOps∧A∈X∧inv⁡G⁡B∈X∧C∈X→AGinv⁡G⁡BHC=AHCGinv⁡G⁡BHC
24 22 23 syldan ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AGinv⁡G⁡BHC=AHCGinv⁡G⁡BHC
25 1 2 3 5 rngoneglmul ⊢R∈RingOps∧B∈X∧C∈X→inv⁡G⁡BHC=inv⁡G⁡BHC
26 25 3adant3r1 ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→inv⁡G⁡BHC=inv⁡G⁡BHC
27 26 oveq2d ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHCGinv⁡G⁡BHC=AHCGinv⁡G⁡BHC
28 24 27 eqtr4d ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AGinv⁡G⁡BHC=AHCGinv⁡G⁡BHC
29 16 28 eqtr4d ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→AHCDBHC=AGinv⁡G⁡BHC
30 8 29 eqtr4d ⊢R∈RingOps∧A∈X∧B∈X∧C∈X→ADBHC=AHCDBHC