Theorem oppglem

Description: Lemma for oppgbas . (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
	oppglem.2	$$⊢E=\mathrm{Slot}N$$
	oppglem.3	$$⊢N\in \mathbb{N}$$
	oppglem.4	$$⊢N\ne 2$$
Assertion	oppglem	$$⊢E\left(R\right)=E\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2		oppglem.2	$$⊢E=\mathrm{Slot}N$$
3		oppglem.3	$$⊢N\in \mathbb{N}$$
4		oppglem.4	$$⊢N\ne 2$$
5	2 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
6	2 3	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
7		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
8	6 7	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\leftrightarrow N\ne 2$$
9	4 8	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
10	5 9	setsnid	$$⊢E\left(R\right)=E\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_R⟩\right)$$
11		eqid	$$⊢{+}_R={+}_R$$
12	11 1	oppgval	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_R⟩$$
13	12	fveq2i	$$⊢E\left(O\right)=E\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_R⟩\right)$$
14	10 13	eqtr4i	$$⊢E\left(R\right)=E\left(O\right)$$