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 ‘ 𝑅 )
	oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
	oppgplusfval.4	⊢ ✚ = ( +g ‘ 𝑂 )
Assertion	oppgplusfval	⊢ ✚ = tpos +

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	⊢ + = ( +g ‘ 𝑅 )
2		oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
3		oppgplusfval.4	⊢ ✚ = ( +g ‘ 𝑂 )
4	1 2	oppgval	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ )
5	4	fveq2i	⊢ ( +g ‘ 𝑂 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) )
6	1	fvexi	⊢ + ∈ V
7	6	tposex	⊢ tpos + ∈ V
8		plusgid	⊢ +g = Slot ( +g ‘ ndx )
9	8	setsid	⊢ ( ( 𝑅 ∈ V ∧ tpos + ∈ V ) → tpos + = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) ) )
10	7 9	mpan2	⊢ ( 𝑅 ∈ V → tpos + = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) ) )
11	5 10	eqtr4id	⊢ ( 𝑅 ∈ V → ( +g ‘ 𝑂 ) = tpos + )
12		tpos0	⊢ tpos ∅ = ∅
13	8	str0	⊢ ∅ = ( +g ‘ ∅ )
14	12 13	eqtr2i	⊢ ( +g ‘ ∅ ) = tpos ∅
15		reldmsets	⊢ Rel dom sSet
16	15	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) = ∅ )
17	4 16	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
18	17	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑂 ) = ( +g ‘ ∅ ) )
19		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑅 ) = ∅ )
20	1 19	syl5eq	⊢ ( ¬ 𝑅 ∈ V → + = ∅ )
21	20	tposeqd	⊢ ( ¬ 𝑅 ∈ V → tpos + = tpos ∅ )
22	14 18 21	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑂 ) = tpos + )
23	11 22	pm2.61i	⊢ ( +g ‘ 𝑂 ) = tpos +
24	3 23	eqtri	⊢ ✚ = tpos +