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 \in RingOps \land (A \in X \land B \in X \land C \in X)) \to 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 \in RingOps \to ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$
5	4	simprd	$⊢ R \in RingOps \to (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))$
6	5	simpld	$⊢ R \in RingOps \to \forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z))$
7		simp2	$⊢ ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \to x H (y G z) = (x H y) G (x H z)$
8	7	ralimi	$⊢ \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \to \forall z \in X x H (y G z) = (x H y) G (x H z)$
9	8	2ralimi	$⊢ \forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \to \forall x \in X \forall y \in X \forall z \in X x H (y G z) = (x H y) G (x H z)$
10		oveq1	$⊢ x = A \to x H (y G z) = A H (y G z)$
11		oveq1	$⊢ x = A \to x H y = A H y$
12		oveq1	$⊢ x = A \to x H z = A H z$
13	11 12	oveq12d	$⊢ x = A \to (x H y) G (x H z) = (A H y) G (A H z)$
14	10 13	eqeq12d	$⊢ x = A \to (x H (y G z) = (x H y) G (x H z) \leftrightarrow A H (y G z) = (A H y) G (A H z))$
15		oveq1	$⊢ y = B \to y G z = B G z$
16	15	oveq2d	$⊢ y = B \to A H (y G z) = A H (B G z)$
17		oveq2	$⊢ y = B \to A H y = A H B$
18	17	oveq1d	$⊢ y = B \to (A H y) G (A H z) = (A H B) G (A H z)$
19	16 18	eqeq12d	$⊢ y = B \to (A H (y G z) = (A H y) G (A H z) \leftrightarrow A H (B G z) = (A H B) G (A H z))$
20		oveq2	$⊢ z = C \to B G z = B G C$
21	20	oveq2d	$⊢ z = C \to A H (B G z) = A H (B G C)$
22		oveq2	$⊢ z = C \to A H z = A H C$
23	22	oveq2d	$⊢ z = C \to (A H B) G (A H z) = (A H B) G (A H C)$
24	21 23	eqeq12d	$⊢ z = C \to (A H (B G z) = (A H B) G (A H z) \leftrightarrow A H (B G C) = (A H B) G (A H C))$
25	14 19 24	rspc3v	$⊢ (A \in X \land B \in X \land C \in X) \to (\forall x \in X \forall y \in X \forall z \in X x H (y G z) = (x H y) G (x H z) \to A H (B G C) = (A H B) G (A H C))$
26	9 25	syl5	$⊢ (A \in X \land B \in X \land C \in X) \to (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \to A H (B G C) = (A H B) G (A H C))$
27	6 26	mpan9	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B G C) = (A H B) G (A H C)$

Metamath Proof Explorer

Theorem rngodi

Proof