Metamath Proof Explorer

Theorem rngoaass

Description: The addition operation of a ring is associative. (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	rngoaass	$⊢ (R \in RingOps \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$

Step	Hyp	Ref	Expression
1		ringgcl.1	$⊢ G = 1^{st} (R)$
2		ringgcl.2	$⊢ X = ran G$
3	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
4	2	grpoass	$⊢ (G \in GrpOp \land (A \in X \land B \in X \land C \in X)) \to (A G B) G C = A G (B G C)$
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 (B G C)$