This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngocom

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	rngocom	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A G B = B G A$

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	ablocom	$⊢ (G \in AbelOp \land A \in X \land B \in X) \to A G B = B G A$
5	3 4	syl3an1	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A G B = B G A$