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 \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (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 \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		simp3	$⊢ ((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 G y) H z = (x H z) G (y 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 G y) H z = (x H z) G (y 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 G y) H z = (x H z) G (y H z)$
10		oveq1	$⊢ x = A \to x G y = A G y$
11	10	oveq1d	$⊢ x = A \to (x G y) H z = (A G y) H z$
12		oveq1	$⊢ x = A \to x H z = A H z$
13	12	oveq1d	$⊢ x = A \to (x H z) G (y H z) = (A H z) G (y H z)$
14	11 13	eqeq12d	$⊢ x = A \to ((x G y) H z = (x H z) G (y H z) \leftrightarrow (A G y) H z = (A H z) G (y H z))$
15		oveq2	$⊢ y = B \to A G y = A G B$
16	15	oveq1d	$⊢ y = B \to (A G y) H z = (A G B) H z$
17		oveq1	$⊢ y = B \to y H z = B H z$
18	17	oveq2d	$⊢ y = B \to (A H z) G (y H z) = (A H z) G (B H z)$
19	16 18	eqeq12d	$⊢ y = B \to ((A G y) H z = (A H z) G (y H z) \leftrightarrow (A G B) H z = (A H z) G (B H z))$
20		oveq2	$⊢ z = C \to (A G B) H z = (A G B) H C$
21		oveq2	$⊢ z = C \to A H z = A H C$
22		oveq2	$⊢ z = C \to B H z = B H C$
23	21 22	oveq12d	$⊢ z = C \to (A H z) G (B H z) = (A H C) G (B H C)$
24	20 23	eqeq12d	$⊢ z = C \to ((A G B) H z = (A H z) G (B H z) \leftrightarrow (A G B) H C = (A H C) G (B 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 G y) H z = (x H z) G (y H z) \to (A G B) H C = (A H C) G (B 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 G B) H C = (A H C) G (B H C))$
27	6 26	mpan9	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A G B) H C = (A H C) G (B H C)$

Metamath Proof Explorer

Theorem rngodir

Proof