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

Metamath Proof Explorer

Theorem oppgplusfval

Description: Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Fan Zheng, 26-Jun-2016)

Ref Expression
Hypotheses oppgval.2 
|- .+ = ( +g ` R )
oppgval.3 
|- O = ( oppG ` R )
oppgplusfval.4 
|- .+b = ( +g ` O )
Assertion oppgplusfval 
|- .+b = tpos .+

Proof

Step Hyp Ref Expression
1 oppgval.2 
 |-  .+ = ( +g ` R )
2 oppgval.3 
 |-  O = ( oppG ` R )
3 oppgplusfval.4 
 |-  .+b = ( +g ` O )
4 1 2 oppgval 
 |-  O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )
5 4 fveq2i 
 |-  ( +g ` O ) = ( +g ` ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
6 1 fvexi 
 |-  .+ e. _V
7 6 tposex 
 |-  tpos .+ e. _V
8 plusgid 
 |-  +g = Slot ( +g ` ndx )
9 8 setsid 
 |-  ( ( R e. _V /\ tpos .+ e. _V ) -> tpos .+ = ( +g ` ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) ) )
10 7 9 mpan2 
 |-  ( R e. _V -> tpos .+ = ( +g ` ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) ) )
11 5 10 eqtr4id 
 |-  ( R e. _V -> ( +g ` O ) = tpos .+ )
12 tpos0 
 |-  tpos (/) = (/)
13 8 str0 
 |-  (/) = ( +g ` (/) )
14 12 13 eqtr2i 
 |-  ( +g ` (/) ) = tpos (/)
15 reldmsets 
 |-  Rel dom sSet
16 15 ovprc1 
 |-  ( -. R e. _V -> ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) = (/) )
17 4 16 eqtrid 
 |-  ( -. R e. _V -> O = (/) )
18 17 fveq2d 
 |-  ( -. R e. _V -> ( +g ` O ) = ( +g ` (/) ) )
19 fvprc 
 |-  ( -. R e. _V -> ( +g ` R ) = (/) )
20 1 19 eqtrid 
 |-  ( -. R e. _V -> .+ = (/) )
21 20 tposeqd 
 |-  ( -. R e. _V -> tpos .+ = tpos (/) )
22 14 18 21 3eqtr4a 
 |-  ( -. R e. _V -> ( +g ` O ) = tpos .+ )
23 11 22 pm2.61i 
 |-  ( +g ` O ) = tpos .+
24 3 23 eqtri 
 |-  .+b = tpos .+