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

Metamath Proof Explorer

Theorem oppgval

Description: Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015) (Revised by Fan Zheng, 26-Jun-2016)

Ref Expression
Hypotheses oppgval.2 
|- .+ = ( +g ` R )
oppgval.3 
|- O = ( oppG ` R )
Assertion oppgval 
|- O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )

Proof

Step Hyp Ref Expression
1 oppgval.2 
 |-  .+ = ( +g ` R )
2 oppgval.3 
 |-  O = ( oppG ` R )
3 id 
 |-  ( x = R -> x = R )
4 fveq2 
 |-  ( x = R -> ( +g ` x ) = ( +g ` R ) )
5 4 1 eqtr4di 
 |-  ( x = R -> ( +g ` x ) = .+ )
6 5 tposeqd 
 |-  ( x = R -> tpos ( +g ` x ) = tpos .+ )
7 6 opeq2d 
 |-  ( x = R -> <. ( +g ` ndx ) , tpos ( +g ` x ) >. = <. ( +g ` ndx ) , tpos .+ >. )
8 3 7 oveq12d 
 |-  ( x = R -> ( x sSet <. ( +g ` ndx ) , tpos ( +g ` x ) >. ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
9 df-oppg 
 |-  oppG = ( x e. _V |-> ( x sSet <. ( +g ` ndx ) , tpos ( +g ` x ) >. ) )
10 ovex 
 |-  ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) e. _V
11 8 9 10 fvmpt 
 |-  ( R e. _V -> ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
12 fvprc 
 |-  ( -. R e. _V -> ( oppG ` R ) = (/) )
13 reldmsets 
 |-  Rel dom sSet
14 13 ovprc1 
 |-  ( -. R e. _V -> ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) = (/) )
15 12 14 eqtr4d 
 |-  ( -. R e. _V -> ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
16 11 15 pm2.61i 
 |-  ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )
17 2 16 eqtri 
 |-  O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )