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

Metamath Proof Explorer

Theorem crngoppr

Description: In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd ). (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses opprval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
opprval.2 ⊢ · = ( .r ‘ 𝑅 )
opprval.3 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprmulfval.4 ⊢ ∙ = ( .r ‘ 𝑂 )
Assertion crngoppr ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∙ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 opprval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 opprval.2 ⊢ · = ( .r ‘ 𝑅 )
3 opprval.3 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
4 opprmulfval.4 ⊢ ∙ = ( .r ‘ 𝑂 )
5 1 2 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )
6 1 2 3 4 opprmul ⊢ ( 𝑋 ∙ 𝑌 ) = ( 𝑌 · 𝑋 )
7 5 6 eqtr4di ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∙ 𝑌 ) )