Metamath Proof Explorer

Theorem rngoa32

Description: The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringgcl.1	$⊢ G = 1^{st} (R)$
	ringgcl.2	$⊢ X = ran G$
Assertion	rngoa32	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = (A G C) G B$

Step	Hyp	Ref	Expression
1		ringgcl.1	$⊢ G = 1^{st} (R)$
2		ringgcl.2	$⊢ X = ran G$
3	1	rngoablo	$⊢ R \in RingOps \to G \in AbelOp$
4	2	ablo32	$⊢ (G \in AbelOp \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = (A G C) G B$
5	3 4	sylan	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = (A G C) G B$