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 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprbas.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion opprbas 𝐵 = ( Base ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 opprbas.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 baseid ⊢ Base = Slot ( Base ‘ ndx )
4 basendxnmulrndx ⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
5 1 3 4 opprlem ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
6 2 5 eqtri ⊢ 𝐵 = ( Base ‘ 𝑂 )