Metamath Proof Explorer


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 + ⟩ )