This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridx 
 |-  .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.