This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crngcomd

Description: Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025)

Ref Expression
Hypotheses crngcomd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
crngcomd.t ⊢ · = ( .r ‘ 𝑅 )
crngcomd.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
crngcomd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
crngcomd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion crngcomd ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 crngcomd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 crngcomd.t ⊢ · = ( .r ‘ 𝑅 )
3 crngcomd.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 crngcomd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 crngcomd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 1 2 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )
7 3 4 5 6 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )