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 ‘ 𝑅 )
	oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
Assertion	oppgval	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ )

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	⊢ + = ( +g ‘ 𝑅 )
2		oppgval.3	⊢ 𝑂 = ( oppg ‘ 𝑅 )
3		id	⊢ ( 𝑥 = 𝑅 → 𝑥 = 𝑅 )
4		fveq2	⊢ ( 𝑥 = 𝑅 → ( +g ‘ 𝑥 ) = ( +g ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑥 = 𝑅 → ( +g ‘ 𝑥 ) = + )
6	5	tposeqd	⊢ ( 𝑥 = 𝑅 → tpos ( +g ‘ 𝑥 ) = tpos + )
7	6	opeq2d	⊢ ( 𝑥 = 𝑅 → ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑥 ) ⟩ = ⟨ ( +g ‘ ndx ) , tpos + ⟩ )
8	3 7	oveq12d	⊢ ( 𝑥 = 𝑅 → ( 𝑥 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑥 ) ⟩ ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) )
9		df-oppg	⊢ oppg = ( 𝑥 ∈ V ↦ ( 𝑥 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑥 ) ⟩ ) )
10		ovex	⊢ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝑅 ∈ V → ( oppg ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) )
12		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( oppg ‘ 𝑅 ) = ∅ )
13		reldmsets	⊢ Rel dom sSet
14	13	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) = ∅ )
15	12 14	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( oppg ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ ) )
16	11 15	pm2.61i	⊢ ( oppg ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ )
17	2 16	eqtri	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos + ⟩ )