Theorem oppgle

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

	Ref	Expression
Hypotheses	oppglt.1	|- O = ( oppG ` R )
	oppgle.2	|- .<_ = ( le ` R )
Assertion	oppgle	|- .<_ = ( le ` O )

Proof

Step	Hyp	Ref	Expression
1		oppglt.1	|- O = ( oppG ` R )
2		oppgle.2	|- .<_ = ( le ` R )
3		eqid	|- ( +g ` R ) = ( +g ` R )
4	3 1	oppgval	|- O = ( R sSet <. ( +g ` ndx ) , tpos ( +g ` R ) >. )
5		pleid	|- le = Slot ( le ` ndx )
6		plendxnplusgndx	|- ( le ` ndx ) =/= ( +g ` ndx )
7	4 5 6	setsplusg	|- ( le ` R ) = ( le ` O )
8	2 7	eqtri	|- .<_ = ( le ` O )