Metamath Proof Explorer


Theorem oppgle

Description: less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses oppglt.1 𝑂 = ( oppg𝑅 )
oppgle.2 = ( le ‘ 𝑅 )
Assertion oppgle = ( le ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppglt.1 𝑂 = ( oppg𝑅 )
2 oppgle.2 = ( le ‘ 𝑅 )
3 eqid ( +g𝑅 ) = ( +g𝑅 )
4 3 1 oppgval 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g𝑅 ) ⟩ )
5 pleid le = Slot ( le ‘ ndx )
6 plendxnplusgndx ( le ‘ ndx ) ≠ ( +g ‘ ndx )
7 4 5 6 setsplusg ( le ‘ 𝑅 ) = ( le ‘ 𝑂 )
8 2 7 eqtri = ( le ‘ 𝑂 )