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

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
18 17 fveq2d ⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑂 ) = ( +g ‘ ∅ ) )
19 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑅 ) = ∅ )
20 1 19 eqtrid ⊢ ( ¬ 𝑅 ∈ 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 +