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 ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 𝑌 ) )