Theorem opprlem

Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	opprlem.2	$$⊢E=\mathrm{Slot}N$$
	opprlem.3	$$⊢N\in \mathbb{N}$$
	opprlem.4	$$⊢N<3$$
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}N$$
3		opprlem.3	$$⊢N\in \mathbb{N}$$
4		opprlem.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)$$