Theorem opprlem

Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by AV, 6-Nov-2024)

	Ref	Expression
Hypotheses	opprbas.1	|- O = ( oppR ` R )
	opprlem.2	|- E = Slot ( E ` ndx )
	opprlem.3	|- ( E ` ndx ) =/= ( .r ` ndx )
Assertion	opprlem	|- ( E ` R ) = ( E ` O )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	|- O = ( oppR ` R )
2		opprlem.2	|- E = Slot ( E ` ndx )
3		opprlem.3	|- ( E ` ndx ) =/= ( .r ` ndx )
4	2 3	setsnid	|- ( E ` R ) = ( E ` ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. ) )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7	5 6 1	opprval	|- O = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. )
8	7	fveq2i	|- ( E ` O ) = ( E ` ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. ) )
9	4 8	eqtr4i	|- ( E ` R ) = ( E ` O )