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 · ⟩ )