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