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 = ( 1st ` R )
	ringgcl.2	|- X = ran G
Assertion	rngoa4	|- ( ( R e. RingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )

Proof

Step	Hyp	Ref	Expression
1		ringgcl.1	|- G = ( 1st ` R )
2		ringgcl.2	|- X = ran G
3	1	rngoablo	|- ( R e. RingOps -> G e. AbelOp )
4	2	ablo4	|- ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
5	3 4	syl3an1	|- ( ( R e. RingOps /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )