crngm23

Description: Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	crngm.1	$⊢ G = 1^{st} (R)$
	crngm.2	$⊢ H = 2^{nd} (R)$
	crngm.3	$⊢ X = ran G$
Assertion	crngm23	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) H C = (A H C) H B$

Step	Hyp	Ref	Expression
1		crngm.1	$⊢ G = 1^{st} (R)$
2		crngm.2	$⊢ H = 2^{nd} (R)$
3		crngm.3	$⊢ X = ran G$
4	1 2 3	crngocom	$⊢ (R \in CRingOps \land B \in X \land C \in X) \to B H C = C H B$
5	4	3adant3r1	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to B H C = C H B$
6	5	oveq2d	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to A H (B H C) = A H (C H B)$
7		crngorngo	$⊢ R \in CRingOps \to R \in RingOps$
8	1 2 3	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)$
9	7 8	sylan	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) H C = A H (B H C)$
10	1 2 3	rngoass	$⊢ (R \in RingOps \land (A \in X \land C \in X \land B \in X)) \to (A H C) H B = A H (C H B)$
11	10	3exp2	$⊢ R \in RingOps \to (A \in X \to (C \in X \to (B \in X \to (A H C) H B = A H (C H B))))$
12	11	com34	$⊢ R \in RingOps \to (A \in X \to (B \in X \to (C \in X \to (A H C) H B = A H (C H B))))$
13	12	3imp2	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A H C) H B = A H (C H B)$
14	7 13	sylan	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to (A H C) H B = A H (C H B)$
15	6 9 14	3eqtr4d	$⊢ (R \in CRingOps \land (A \in X \land B \in X \land C \in X)) \to (A H B) H C = (A H C) H B$

Metamath Proof Explorer