Theorem opprlem

Description: Lemma for opprbas and oppradd . (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprbas.1	|- O = ( oppR ` R )
	opprlem.2	|- E = Slot N
	opprlem.3	|- N e. NN
	opprlem.4	|- N < 3
Assertion	opprlem	|- ( E ` R ) = ( E ` O )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	|- O = ( oppR ` R )
2		opprlem.2	|- E = Slot N
3		opprlem.3	|- N e. NN
4		opprlem.4	|- N < 3
5	2 3	ndxid	|- E = Slot ( E ` ndx )
6	3	nnrei	|- N e. RR
7	6 4	ltneii	|- N =/= 3
8	2 3	ndxarg	|- ( E ` ndx ) = N
9		mulrndx	|- ( .r ` ndx ) = 3
10	8 9	neeq12i	|- ( ( E ` ndx ) =/= ( .r ` ndx ) <-> N =/= 3 )
11	7 10	mpbir	|- ( E ` ndx ) =/= ( .r ` ndx )
12	5 11	setsnid	|- ( E ` R ) = ( E ` ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. ) )
13		eqid	|- ( Base ` R ) = ( Base ` R )
14		eqid	|- ( .r ` R ) = ( .r ` R )
15	13 14 1	opprval	|- O = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. )
16	15	fveq2i	|- ( E ` O ) = ( E ` ( R sSet <. ( .r ` ndx ) , tpos ( .r ` R ) >. ) )
17	12 16	eqtr4i	|- ( E ` R ) = ( E ` O )