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 ⁡ R
ringsubdi.2 ⊢ H = 2 nd ⁡ R
ringsubdi.3 ⊢ X = ran ⁡ G
ringsubdi.4 ⊢ D = / g ⁡ G
Assertion rngosubdir ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B H C = A H C D B H C

Proof

Step Hyp Ref Expression
1 ringsubdi.1 ⊢ G = 1 st ⁡ R
2 ringsubdi.2 ⊢ H = 2 nd ⁡ 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 → A D B = A G inv ⁡ G ⁡ B
7 6 3adant3r3 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B = A G inv ⁡ G ⁡ B
8 7 oveq1d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B H C = A G inv ⁡ G ⁡ B H C
9 1 2 3 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ C ∈ X → A H C ∈ X
10 9 3adant3r2 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C ∈ X
11 1 2 3 rngocl ⊢ R ∈ RingOps ∧ B ∈ X ∧ C ∈ X → B H C ∈ X
12 11 3adant3r1 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B H C ∈ X
13 10 12 jca ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C ∈ X ∧ B H C ∈ X
14 1 3 5 4 rngosub ⊢ R ∈ RingOps ∧ A H C ∈ X ∧ B H C ∈ X → A H C D B H C = A H C G inv ⁡ G ⁡ B H C
15 14 3expb ⊢ R ∈ RingOps ∧ A H C ∈ X ∧ B H C ∈ X → A H C D B H C = A H C G inv ⁡ G ⁡ B H C
16 13 15 syldan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C D B H C = A H C G inv ⁡ G ⁡ B H C
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 → A G inv ⁡ G ⁡ B H C = A H C G inv ⁡ G ⁡ B H C
24 22 23 syldan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G inv ⁡ G ⁡ B H C = A H C G inv ⁡ G ⁡ B H C
25 1 2 3 5 rngoneglmul ⊢ R ∈ RingOps ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ B H C = inv ⁡ G ⁡ B H C
26 25 3adant3r1 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → inv ⁡ G ⁡ B H C = inv ⁡ G ⁡ B H C
27 26 oveq2d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C G inv ⁡ G ⁡ B H C = A H C G inv ⁡ G ⁡ B H C
28 24 27 eqtr4d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G inv ⁡ G ⁡ B H C = A H C G inv ⁡ G ⁡ B H C
29 16 28 eqtr4d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C D B H C = A G inv ⁡ G ⁡ B H C
30 8 29 eqtr4d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B H C = A H C D B H C