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

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 mulridx ⊢ .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 ·