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	$$⊢\underset{\dot{}}{+}={+}_R$$
	oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
	oppgplusfval.4	$$⊢\underset{\dot{}}{✚}={+}_O$$
Assertion	oppgplusfval	$$⊢\underset{\dot{}}{✚}=tpos\underset{\dot{}}{+}$$

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	$$⊢\underset{\dot{}}{+}={+}_R$$
2		oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
3		oppgplusfval.4	$$⊢\underset{\dot{}}{✚}={+}_O$$
4	1 2	oppgval	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
5	4	fveq2i	$$⊢{+}_O={+}_{\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩\right)}$$
6	1	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
7	6	tposex	$$⊢tpos\underset{\dot{}}{+}\in \mathrm{V}$$
8		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
9	8	setsid	$$⊢\left(R\in \mathrm{V}\wedge tpos\underset{\dot{}}{+}\in \mathrm{V}\right)\to tpos\underset{\dot{}}{+}={+}_{\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩\right)}$$
10	7 9	mpan2	$$⊢R\in \mathrm{V}\to tpos\underset{\dot{}}{+}={+}_{\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩\right)}$$
11	5 10	eqtr4id	$$⊢R\in \mathrm{V}\to {+}_O=tpos\underset{\dot{}}{+}$$
12		tpos0	$$⊢tpos\varnothing =\varnothing$$
13	8	str0	$$⊢\varnothing ={+}_{\varnothing }$$
14	12 13	eqtr2i	$$⊢{+}_{\varnothing }=tpos\varnothing$$
15		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
16	15	ovprc1	$$⊢\neg R\in \mathrm{V}\to R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩=\varnothing$$
17	4 16	syl5eq	$$⊢\neg R\in \mathrm{V}\to O=\varnothing$$
18	17	fveq2d	$$⊢\neg R\in \mathrm{V}\to {+}_O={+}_{\varnothing }$$
19		fvprc	$$⊢\neg R\in \mathrm{V}\to {+}_R=\varnothing$$
20	1 19	syl5eq	$$⊢\neg R\in \mathrm{V}\to \underset{\dot{}}{+}=\varnothing$$
21	20	tposeqd	$$⊢\neg R\in \mathrm{V}\to tpos\underset{\dot{}}{+}=tpos\varnothing$$
22	14 18 21	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {+}_O=tpos\underset{\dot{}}{+}$$
23	11 22	pm2.61i	$$⊢{+}_O=tpos\underset{\dot{}}{+}$$
24	3 23	eqtri	$$⊢\underset{\dot{}}{✚}=tpos\underset{\dot{}}{+}$$