Theorem opprmulfval

Description: Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprval.1	|- B = ( Base ` R )
	opprval.2	|- .x. = ( .r ` R )
	opprval.3	|- O = ( oppR ` R )
	opprmulfval.4	|- .xb = ( .r ` O )
Assertion	opprmulfval	|- .xb = tpos .x.

Proof

Step	Hyp	Ref	Expression
1		opprval.1	|- B = ( Base ` R )
2		opprval.2	|- .x. = ( .r ` R )
3		opprval.3	|- O = ( oppR ` R )
4		opprmulfval.4	|- .xb = ( .r ` O )
5	1 2 3	opprval	|- O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )
6	5	fveq2i	|- ( .r ` O ) = ( .r ` ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
7	2	fvexi	|- .x. e. _V
8	7	tposex	|- tpos .x. e. _V
9		mulrid	|- .r = Slot ( .r ` ndx )
10	9	setsid	|- ( ( R e. _V /\ tpos .x. e. _V ) -> tpos .x. = ( .r ` ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) ) )
11	8 10	mpan2	|- ( R e. _V -> tpos .x. = ( .r ` ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) ) )
12	6 11	eqtr4id	|- ( R e. _V -> ( .r ` O ) = tpos .x. )
13		tpos0	|- tpos (/) = (/)
14	9	str0	|- (/) = ( .r ` (/) )
15	13 14	eqtr2i	|- ( .r ` (/) ) = tpos (/)
16		fvprc	|- ( -. R e. _V -> ( oppR ` R ) = (/) )
17	3 16	eqtrid	|- ( -. R e. _V -> O = (/) )
18	17	fveq2d	|- ( -. R e. _V -> ( .r ` O ) = ( .r ` (/) ) )
19		fvprc	|- ( -. R e. _V -> ( .r ` R ) = (/) )
20	2 19	eqtrid	|- ( -. R e. _V -> .x. = (/) )
21	20	tposeqd	|- ( -. R e. _V -> tpos .x. = tpos (/) )
22	15 18 21	3eqtr4a	|- ( -. R e. _V -> ( .r ` O ) = tpos .x. )
23	12 22	pm2.61i	|- ( .r ` O ) = tpos .x.
24	4 23	eqtri	|- .xb = tpos .x.