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

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 ⊢ O = opp 𝑔 ⁡ R
oppgle.2 ⊢ ≤ ˙ = ≤ R
Assertion oppgle ⊢ ≤ ˙ = ≤ O

Proof

Step Hyp Ref Expression
1 oppglt.1 ⊢ O = opp 𝑔 ⁡ R
2 oppgle.2 ⊢ ≤ ˙ = ≤ R
3 eqid ⊢ + R = + R
4 3 1 oppgval ⊢ O = R sSet + ndx tpos + R
5 pleid ⊢ le = Slot ≤ ndx
6 plendxnplusgndx ⊢ ≤ ndx ≠ + ndx
7 4 5 6 setsplusg ⊢ ≤ R = ≤ O
8 2 7 eqtri ⊢ ≤ ˙ = ≤ O