Metamath Proof Explorer

Theorem rngoa4

Description: Rearrangement of 4 terms in a sum of ring elements. (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	rngoa4	$⊢ (R \in RingOps \land (A \in X \land B \in X) \land (C \in X \land D \in X)) \to (A G B) G (C G D) = (A G C) G (B G D)$

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