Theorem cringmul32d

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

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

Proof

Step	Hyp	Ref	Expression
1		cringmul32d.b	|- B = ( Base ` R )
2		cringmul32d.t	|- .x. = ( .r ` R )
3		cringmul32d.r	|- ( ph -> R e. CRing )
4		cringmul32d.x	|- ( ph -> X e. B )
5		cringmul32d.y	|- ( ph -> Y e. B )
6		cringmul32d.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 ) )