Theorem mgplem

Description: Lemma for mgpbas . (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
	mgplem.2	$$⊢E=\mathrm{Slot}N$$
	mgplem.3	$$⊢N\in \mathbb{N}$$
	mgplem.4	$$⊢N\ne 2$$
Assertion	mgplem	$$⊢E\left(R\right)=E\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	$$⊢M={\mathrm{mulGrp}}_R$$
2		mgplem.2	$$⊢E=\mathrm{Slot}N$$
3		mgplem.3	$$⊢N\in \mathbb{N}$$
4		mgplem.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}},{\cdot }_R⟩\right)$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12	1 11	mgpval	$$⊢M=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_R⟩$$
13	12	fveq2i	$$⊢E\left(M\right)=E\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_R⟩\right)$$
14	10 13	eqtr4i	$$⊢E\left(R\right)=E\left(M\right)$$