Theorem mgplem

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

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

Proof

Step	Hyp	Ref	Expression
1		mgpbas.1	|- M = ( mulGrp ` R )
2		mgplem.2	|- E = Slot N
3		mgplem.3	|- N e. NN
4		mgplem.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 )