Theorem oppglemOLD

Description: Obsolete version of setsplusg as of 18-Oct-2024. Lemma for oppgbas . (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2		oppglemOLD.2	$$⊢E=\mathrm{Slot}N$$
3		oppglemOLD.3	$$⊢N\in \mathbb{N}$$
4		oppglemOLD.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)$$