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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	crng32d.t	⊢ · = ( .r ‘ 𝑅 )
	crng32d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	crng32d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	crng32d.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	crng32d.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	crng4.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
Assertion	crng4	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · ( 𝑍 · 𝑈 ) ) = ( ( 𝑋 · 𝑍 ) · ( 𝑌 · 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		crng32d.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		crng32d.t	⊢ · = ( .r ‘ 𝑅 )
3		crng32d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		crng32d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		crng32d.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		crng32d.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		crng4.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
8	1 2 3 4 5 6	crng32d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) · 𝑌 ) )
9	8	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) · 𝑍 ) · 𝑈 ) = ( ( ( 𝑋 · 𝑍 ) · 𝑌 ) · 𝑈 ) )
10	3	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
11	1 2 10 4 5	ringcld	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
12	1 2 10 11 6 7	ringassd	⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) · 𝑍 ) · 𝑈 ) = ( ( 𝑋 · 𝑌 ) · ( 𝑍 · 𝑈 ) ) )
13	1 2 10 4 6	ringcld	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
14	1 2 10 13 5 7	ringassd	⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑍 ) · 𝑌 ) · 𝑈 ) = ( ( 𝑋 · 𝑍 ) · ( 𝑌 · 𝑈 ) ) )
15	9 12 14	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · ( 𝑍 · 𝑈 ) ) = ( ( 𝑋 · 𝑍 ) · ( 𝑌 · 𝑈 ) ) )