Theorem crng32d

Description: Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32d . (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	crng32d.b	|- B = ( Base ` R )
	crng32d.t	|- .x. = ( .r ` R )
	crng32d.r	|- ( ph -> R e. CRing )
	crng32d.x	|- ( ph -> X e. B )
	crng32d.y	|- ( ph -> Y e. B )
	crng32d.z	|- ( ph -> Z e. B )
Assertion	crng32d	|- ( ph -> ( ( X .x. Y ) .x. Z ) = ( ( X .x. Z ) .x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		crng32d.b	|- B = ( Base ` R )
2		crng32d.t	|- .x. = ( .r ` R )
3		crng32d.r	|- ( ph -> R e. CRing )
4		crng32d.x	|- ( ph -> X e. B )
5		crng32d.y	|- ( ph -> Y e. B )
6		crng32d.z	|- ( ph -> Z e. B )
7	1 2 3 5 6	crngcomd	|- ( ph -> ( Y .x. Z ) = ( Z .x. Y ) )
8	7	oveq2d	|- ( ph -> ( X .x. ( Y .x. Z ) ) = ( X .x. ( Z .x. Y ) ) )
9	3	crngringd	|- ( ph -> R e. Ring )
10	1 2 9 4 5 6	ringassd	|- ( ph -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
11	1 2 9 4 6 5	ringassd	|- ( ph -> ( ( X .x. Z ) .x. Y ) = ( X .x. ( Z .x. Y ) ) )
12	8 10 11	3eqtr4d	|- ( ph -> ( ( X .x. Y ) .x. Z ) = ( ( X .x. Z ) .x. Y ) )