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

Metamath Proof Explorer

Theorem oppgbas

Description: Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypotheses oppgbas.1 ⊢ O = opp 𝑔 ⁡ R
oppgbas.2 ⊢ B = Base R
Assertion oppgbas ⊢ B = Base O

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ O = opp 𝑔 ⁡ R
2 oppgbas.2 ⊢ B = Base R
3 eqid ⊢ + R = + R
4 3 1 oppgval ⊢ O = R sSet + ndx tpos + R
5 baseid ⊢ Base = Slot Base ndx
6 basendxnplusgndx ⊢ Base ndx ≠ + ndx
7 4 5 6 setsplusg ⊢ Base R = Base O
8 2 7 eqtri ⊢ B = Base O