rngoass

Description: Associative law for the multiplication operation of a ring. (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	rngoass	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) H C = A H (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		simp1	$⊢ ((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) H z = x H (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 H y) H z = x H (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 H y) H z = x H (y H z)$
10	6 9	syl	$⊢ 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)$
11		oveq1	$⊢ x = A \to x H y = A H y$
12	11	oveq1d	$⊢ x = A \to (x H y) H z = (A H y) H z$
13		oveq1	$⊢ x = A \to x H (y H z) = A H (y H z)$
14	12 13	eqeq12d	$⊢ x = A \to ((x H y) H z = x H (y H z) \leftrightarrow (A H y) H z = A H (y H z))$
15		oveq2	$⊢ y = B \to A H y = A H B$
16	15	oveq1d	$⊢ y = B \to (A H y) H z = (A H B) H z$
17		oveq1	$⊢ y = B \to y H z = B H z$
18	17	oveq2d	$⊢ y = B \to A H (y H z) = A H (B H z)$
19	16 18	eqeq12d	$⊢ y = B \to ((A H y) H z = A H (y H z) \leftrightarrow (A H B) H z = A H (B H z))$
20		oveq2	$⊢ z = C \to (A H B) H z = (A H B) H C$
21		oveq2	$⊢ z = C \to B H z = B H C$
22	21	oveq2d	$⊢ z = C \to A H (B H z) = A H (B H C)$
23	20 22	eqeq12d	$⊢ z = C \to ((A H B) H z = A H (B H z) \leftrightarrow (A H B) H C = A H (B H C))$
24	14 19 23	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) H z = x H (y H z) \to (A H B) H C = A H (B H C))$
25	10 24	mpan9	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) H C = A H (B H C)$

Metamath Proof Explorer

Theorem rngoass

Proof