Theorem crng4

Description: Commutative/associative law for commutative rings. See also mul4d . (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 20-Jul-2026)

	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 )
	crng4.u	|- ( ph -> U e. B )
Assertion	crng4	|- ( ph -> ( ( X .x. Y ) .x. ( Z .x. U ) ) = ( ( X .x. Z ) .x. ( Y .x. U ) ) )

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		crng4.u	|- ( ph -> U e. B )
8	1 2 3 4 5 6	crng32d	|- ( ph -> ( ( X .x. Y ) .x. Z ) = ( ( X .x. Z ) .x. Y ) )
9	8	oveq1d	|- ( ph -> ( ( ( X .x. Y ) .x. Z ) .x. U ) = ( ( ( X .x. Z ) .x. Y ) .x. U ) )
10	3	crngringd	|- ( ph -> R e. Ring )
11	1 2 10 4 5	ringcld	|- ( ph -> ( X .x. Y ) e. B )
12	1 2 10 11 6 7	ringassd	|- ( ph -> ( ( ( X .x. Y ) .x. Z ) .x. U ) = ( ( X .x. Y ) .x. ( Z .x. U ) ) )
13	1 2 10 4 6	ringcld	|- ( ph -> ( X .x. Z ) e. B )
14	1 2 10 13 5 7	ringassd	|- ( ph -> ( ( ( X .x. Z ) .x. Y ) .x. U ) = ( ( X .x. Z ) .x. ( Y .x. U ) ) )
15	9 12 14	3eqtr3d	|- ( ph -> ( ( X .x. Y ) .x. ( Z .x. U ) ) = ( ( X .x. Z ) .x. ( Y .x. U ) ) )