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={opp}_r\left(R\right)$$
	opprlem.2	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	opprlem.3	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
Assertion	opprlem	$$⊢E\left(R\right)=E\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2		opprlem.2	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
3		opprlem.3	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
4	2 3	setsnid	$$⊢E\left(R\right)=E\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩\right)$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	5 6 1	opprval	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩$$
8	7	fveq2i	$$⊢E\left(O\right)=E\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩\right)$$
9	4 8	eqtr4i	$$⊢E\left(R\right)=E\left(O\right)$$