Theorem opprlemOLD

Description: Obsolete version of opprlem as of 6-Nov-2024. Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	opprlemOLD.2	$$⊢E=\mathrm{Slot}N$$
	opprlemOLD.3	$$⊢N\in \mathbb{N}$$
	opprlemOLD.4	$$⊢N<3$$
Assertion	opprlemOLD	$$⊢E\left(R\right)=E\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2		opprlemOLD.2	$$⊢E=\mathrm{Slot}N$$
3		opprlemOLD.3	$$⊢N\in \mathbb{N}$$
4		opprlemOLD.4	$$⊢N<3$$
5	2 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
6	3	nnrei	$$⊢N\in ℝ$$
7	6 4	ltneii	$$⊢N\ne 3$$
8	2 3	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
9		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
10	8 9	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow N\ne 3$$
11	7 10	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
12	5 11	setsnid	$$⊢E\left(R\right)=E\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩\right)$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14		eqid	$$⊢{\cdot }_R={\cdot }_R$$
15	13 14 1	opprval	$$⊢O=R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩$$
16	15	fveq2i	$$⊢E\left(O\right)=E\left(R\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_R⟩\right)$$
17	12 16	eqtr4i	$$⊢E\left(R\right)=E\left(O\right)$$