Theorem mgplemOLD

Description: Obsolete version of setsplusg as of 18-Oct-2024. Lemma for mgpbas . (Contributed by Mario Carneiro, 5-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mgpbas.1	|- M = ( mulGrp ` R )
	mgplemOLD.2	|- E = Slot N
	mgplemOLD.3	|- N e. NN
	mgplemOLD.4	|- N =/= 2
Assertion	mgplemOLD	|- ( E ` R ) = ( E ` M )

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	|- M = ( mulGrp ` R )
2		mgplemOLD.2	|- E = Slot N
3		mgplemOLD.3	|- N e. NN
4		mgplemOLD.4	|- N =/= 2
5	2 3	ndxid	|- E = Slot ( E ` ndx )
6	2 3	ndxarg	|- ( E ` ndx ) = N
7		plusgndx	|- ( +g ` ndx ) = 2
8	6 7	neeq12i	|- ( ( E ` ndx ) =/= ( +g ` ndx ) <-> N =/= 2 )
9	4 8	mpbir	|- ( E ` ndx ) =/= ( +g ` ndx )
10	5 9	setsnid	|- ( E ` R ) = ( E ` ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
11		eqid	|- ( .r ` R ) = ( .r ` R )
12	1 11	mgpval	|- M = ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. )
13	12	fveq2i	|- ( E ` M ) = ( E ` ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
14	10 13	eqtr4i	|- ( E ` R ) = ( E ` M )