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	syl5eq	|- ( -. R e. _V -> O = (/) )
18	17	fveq2d	|- ( -. R e. _V -> ( +g ` O ) = ( +g ` (/) ) )
19		fvprc	|- ( -. R e. _V -> ( +g ` R ) = (/) )
20	1 19	syl5eq	|- ( -. 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 .+