This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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