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