Metamath Proof Explorer

Theorem rngodi

Description: Distributive law for the multiplication operation of a ring (left-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 rngodi ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B G C = A H B G A 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 simp2 ⊢ 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 H y G z = x H y G x 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 H y G z = x H y G x 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 H y G z = x H y G x H z
10 oveq1 ⊢ x = A → x H y G z = A H y G z
11 oveq1 ⊢ x = A → x H y = A H y
12 oveq1 ⊢ x = A → x H z = A H z
13 11 12 oveq12d ⊢ x = A → x H y G x H z = A H y G A H z
14 10 13 eqeq12d ⊢ x = A → x H y G z = x H y G x H z ↔ A H y G z = A H y G A H z
15 oveq1 ⊢ y = B → y G z = B G z
16 15 oveq2d ⊢ y = B → A H y G z = A H B G z
17 oveq2 ⊢ y = B → A H y = A H B
18 17 oveq1d ⊢ y = B → A H y G A H z = A H B G A H z
19 16 18 eqeq12d ⊢ y = B → A H y G z = A H y G A H z ↔ A H B G z = A H B G A H z
20 oveq2 ⊢ z = C → B G z = B G C
21 20 oveq2d ⊢ z = C → A H B G z = A H B G C
22 oveq2 ⊢ z = C → A H z = A H C
23 22 oveq2d ⊢ z = C → A H B G A H z = A H B G A H C
24 21 23 eqeq12d ⊢ z = C → A H B G z = A H B G A H z ↔ A H B G C = A H B G A H C
25 14 19 24 rspc3v ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x H y G z = x H y G x H z → A H B G C = A H B G A 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 H B G C = A H B G A H C
27 6 26 mpan9 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B G C = A H B G A H C