Metamath Proof Explorer

Theorem rngodir

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 ⊢ G = 1 st ⁡ R
ringi.2 ⊢ H = 2 nd ⁡ R
ringi.3 ⊢ X = ran ⁡ G
Assertion rngodir ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B H C = A H C G B H C

Proof

Step Hyp Ref Expression
1 ringi.1 ⊢ G = 1 st ⁡ R
2 ringi.2 ⊢ H = 2 nd ⁡ R
3 ringi.3 ⊢ X = ran ⁡ G
4 1 2 3 rngoi ⊢ R ∈ RingOps → G ∈ AbelOp ∧ H : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y
5 4 simprd ⊢ R ∈ RingOps → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z ∧ ∃ x ∈ X ∀ y ∈ X x H y = y ∧ y H x = y
6 5 simpld ⊢ R ∈ RingOps → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z
7 simp3 ⊢ x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z → x G y H z = x H z G y H z
8 7 ralimi ⊢ ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z → ∀ z ∈ X x G y H z = x H z G y H z
9 8 2ralimi ⊢ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y H z = x H z G y H z
10 oveq1 ⊢ x = A → x G y = A G y
11 10 oveq1d ⊢ x = A → x G y H z = A G y H z
12 oveq1 ⊢ x = A → x H z = A H z
13 12 oveq1d ⊢ x = A → x H z G y H z = A H z G y H z
14 11 13 eqeq12d ⊢ x = A → x G y H z = x H z G y H z ↔ A G y H z = A H z G y H z
15 oveq2 ⊢ y = B → A G y = A G B
16 15 oveq1d ⊢ y = B → A G y H z = A G B H z
17 oveq1 ⊢ y = B → y H z = B H z
18 17 oveq2d ⊢ y = B → A H z G y H z = A H z G B H z
19 16 18 eqeq12d ⊢ y = B → A G y H z = A H z G y H z ↔ A G B H z = A H z G B H z
20 oveq2 ⊢ z = C → A G B H z = A G B H C
21 oveq2 ⊢ z = C → A H z = A H C
22 oveq2 ⊢ z = C → B H z = B H C
23 21 22 oveq12d ⊢ z = C → A H z G B H z = A H C G B H C
24 20 23 eqeq12d ⊢ z = C → A G B H z = A H z G B H z ↔ A G B H C = A H C G B H C
25 14 19 24 rspc3v ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y H z = x H z G y H z → A G B H C = A H C G B H C
26 9 25 syl5 ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y H z = x H y H z ∧ x H y G z = x H y G x H z ∧ x G y H z = x H z G y H z → A G B H C = A H C G B H C
27 6 26 mpan9 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B H C = A H C G B H C