Metamath Proof Explorer

Theorem opprval

Description: Value of the 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 )
Assertion opprval 
|- O = ( R sSet <. ( .r ` ndx ) , 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 id 
 |-  ( x = R -> x = R )
5 fveq2 
 |-  ( x = R -> ( .r ` x ) = ( .r ` R ) )
6 5 2 eqtr4di 
 |-  ( x = R -> ( .r ` x ) = .x. )
7 6 tposeqd 
 |-  ( x = R -> tpos ( .r ` x ) = tpos .x. )
8 7 opeq2d 
 |-  ( x = R -> <. ( .r ` ndx ) , tpos ( .r ` x ) >. = <. ( .r ` ndx ) , tpos .x. >. )
9 4 8 oveq12d 
 |-  ( x = R -> ( x sSet <. ( .r ` ndx ) , tpos ( .r ` x ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
10 df-oppr 
 |-  oppR = ( x e. _V |-> ( x sSet <. ( .r ` ndx ) , tpos ( .r ` x ) >. ) )
11 ovex 
 |-  ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) e. _V
12 9 10 11 fvmpt 
 |-  ( R e. _V -> ( oppR ` R ) = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
13 fvprc 
 |-  ( -. R e. _V -> ( oppR ` R ) = (/) )
14 reldmsets 
 |-  Rel dom sSet
15 14 ovprc1 
 |-  ( -. R e. _V -> ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) = (/) )
16 13 15 eqtr4d 
 |-  ( -. R e. _V -> ( oppR ` R ) = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
17 12 16 pm2.61i 
 |-  ( oppR ` R ) = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )
18 3 17 eqtri 
 |-  O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )