Theorem crng12d

Description: Commutative/associative law that swaps the first two factors in a triple product in a commutative ring. See also mul12d . (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypotheses	crng12d.b	|- B = ( Base ` R )
	crng12d.t	|- .x. = ( .r ` R )
	crng12d.r	|- ( ph -> R e. CRing )
	crng12d.1	|- ( ph -> X e. B )
	crng12d.2	|- ( ph -> Y e. B )
	crng12d.3	|- ( ph -> Z e. B )
Assertion	crng12d	|- ( ph -> ( X .x. ( Y .x. Z ) ) = ( Y .x. ( X .x. Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		crng12d.b	|- B = ( Base ` R )
2		crng12d.t	|- .x. = ( .r ` R )
3		crng12d.r	|- ( ph -> R e. CRing )
4		crng12d.1	|- ( ph -> X e. B )
5		crng12d.2	|- ( ph -> Y e. B )
6		crng12d.3	|- ( ph -> Z e. B )
7	1 2 3 4 5	crngcomd	|- ( ph -> ( X .x. Y ) = ( Y .x. X ) )
8	7	oveq1d	|- ( ph -> ( ( X .x. Y ) .x. Z ) = ( ( Y .x. X ) .x. Z ) )
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 5 4 6	ringassd	|- ( ph -> ( ( Y .x. X ) .x. Z ) = ( Y .x. ( X .x. Z ) ) )
12	8 10 11	3eqtr3d	|- ( ph -> ( X .x. ( Y .x. Z ) ) = ( Y .x. ( X .x. Z ) ) )