Database
BASIC ALGEBRAIC STRUCTURES
Rings
Opposite ring
crngoppr
Metamath Proof Explorer
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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∙ 𝑌 ) )