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 𝑂 = ( oppg𝑅 )
oppgbas.2 𝐵 = ( Base ‘ 𝑅 )
Assertion oppgbas 𝐵 = ( Base ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppgbas.1 𝑂 = ( oppg𝑅 )
2 oppgbas.2 𝐵 = ( Base ‘ 𝑅 )
3 eqid ( +g𝑅 ) = ( +g𝑅 )
4 3 1 oppgval 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g𝑅 ) ⟩ )
5 baseid Base = Slot ( Base ‘ ndx )
6 basendxnplusgndx ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
7 4 5 6 setsplusg ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
8 2 7 eqtri 𝐵 = ( Base ‘ 𝑂 )