Metamath Proof Explorer


Theorem opprmulfval

Description: Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprval.1 𝐵 = ( Base ‘ 𝑅 )
opprval.2 · = ( .r𝑅 )
opprval.3 𝑂 = ( oppr𝑅 )
opprmulfval.4 = ( .r𝑂 )
Assertion opprmulfval = tpos ·

Proof

Step Hyp Ref Expression
1 opprval.1 𝐵 = ( Base ‘ 𝑅 )
2 opprval.2 · = ( .r𝑅 )
3 opprval.3 𝑂 = ( oppr𝑅 )
4 opprmulfval.4 = ( .r𝑂 )
5 1 2 3 opprval 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
6 5 fveq2i ( .r𝑂 ) = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
7 2 fvexi · ∈ V
8 7 tposex tpos · ∈ V
9 mulrid .r = Slot ( .r ‘ ndx )
10 9 setsid ( ( 𝑅 ∈ V ∧ tpos · ∈ V ) → tpos · = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ) )
11 8 10 mpan2 ( 𝑅 ∈ V → tpos · = ( .r ‘ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ) )
12 6 11 eqtr4id ( 𝑅 ∈ V → ( .r𝑂 ) = tpos · )
13 tpos0 tpos ∅ = ∅
14 9 str0 ∅ = ( .r ‘ ∅ )
15 13 14 eqtr2i ( .r ‘ ∅ ) = tpos ∅
16 fvprc ( ¬ 𝑅 ∈ V → ( oppr𝑅 ) = ∅ )
17 3 16 eqtrid ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
18 17 fveq2d ( ¬ 𝑅 ∈ V → ( .r𝑂 ) = ( .r ‘ ∅ ) )
19 fvprc ( ¬ 𝑅 ∈ V → ( .r𝑅 ) = ∅ )
20 2 19 eqtrid ( ¬ 𝑅 ∈ V → · = ∅ )
21 20 tposeqd ( ¬ 𝑅 ∈ V → tpos · = tpos ∅ )
22 15 18 21 3eqtr4a ( ¬ 𝑅 ∈ V → ( .r𝑂 ) = tpos · )
23 12 22 pm2.61i ( .r𝑂 ) = tpos ·
24 4 23 eqtri = tpos ·