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

Metamath Proof Explorer

Theorem opprbas

Description: Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014) (Proof shortened by AV, 6-Nov-2024)

Ref Expression
Hypotheses opprbas.1 ⊢ O = opp r ⁡ R
opprbas.2 ⊢ B = Base R
Assertion opprbas ⊢ B = Base O

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ O = opp r ⁡ R
2 opprbas.2 ⊢ B = Base R
3 baseid ⊢ Base = Slot Base ndx
4 basendxnmulrndx ⊢ Base ndx ≠ ⋅ ndx
5 1 3 4 opprlem ⊢ Base R = Base O
6 2 5 eqtri ⊢ B = Base O