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

Metamath Proof Explorer

Theorem opprval

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

Ref Expression
Hypotheses opprval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
opprval.2 ⊢ · = ( .r ‘ 𝑅 )
opprval.3 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprval 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )

Proof

Step Hyp Ref Expression
1 opprval.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 opprval.2 ⊢ · = ( .r ‘ 𝑅 )
3 opprval.3 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
4 id ⊢ ( 𝑥 = 𝑅 → 𝑥 = 𝑅 )
5 fveq2 ⊢ ( 𝑥 = 𝑅 → ( .r ‘ 𝑥 ) = ( .r ‘ 𝑅 ) )
6 5 2 eqtr4di ⊢ ( 𝑥 = 𝑅 → ( .r ‘ 𝑥 ) = · )
7 6 tposeqd ⊢ ( 𝑥 = 𝑅 → tpos ( .r ‘ 𝑥 ) = tpos · )
8 7 opeq2d ⊢ ( 𝑥 = 𝑅 → ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ = ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
9 4 8 oveq12d ⊢ ( 𝑥 = 𝑅 → ( 𝑥 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
10 df-oppr ⊢ oppr = ( 𝑥 ∈ V ↦ ( 𝑥 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ ) )
11 ovex ⊢ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ∈ V
12 9 10 11 fvmpt ⊢ ( 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
13 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ∅ )
14 reldmsets ⊢ Rel dom sSet
15 14 ovprc1 ⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) = ∅ )
16 13 15 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
17 12 16 pm2.61i ⊢ ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
18 3 17 eqtri ⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )