Metamath Proof Explorer

Theorem opprabs

Description: The opposite ring of the opposite ring is the original ring. Note the conditions on this theorem, which makes it unpractical in case we only have e.g. R e. Ring as a premise. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses opprabs.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
opprabs.m ⊢ · = ( .r ‘ 𝑅 )
opprabs.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
opprabs.2 ⊢ ( 𝜑 → Fun 𝑅 )
opprabs.3 ⊢ ( 𝜑 → ( .r ‘ ndx ) ∈ dom 𝑅 )
opprabs.4 ⊢ ( 𝜑 → · Fn ( 𝐵 × 𝐵 ) )
Assertion opprabs ( 𝜑 → 𝑅 = ( oppr ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 opprabs.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 opprabs.m ⊢ · = ( .r ‘ 𝑅 )
3 opprabs.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 opprabs.2 ⊢ ( 𝜑 → Fun 𝑅 )
5 opprabs.3 ⊢ ( 𝜑 → ( .r ‘ ndx ) ∈ dom 𝑅 )
6 opprabs.4 ⊢ ( 𝜑 → · Fn ( 𝐵 × 𝐵 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
9 7 2 1 8 opprmulfval ⊢ ( .r ‘ 𝑂 ) = tpos ·
10 9 tposeqi ⊢ tpos ( .r ‘ 𝑂 ) = tpos tpos ·
11 fnrel ⊢ ( · Fn ( 𝐵 × 𝐵 ) → Rel · )
12 relxp ⊢ Rel ( 𝐵 × 𝐵 )
13 fndm ⊢ ( · Fn ( 𝐵 × 𝐵 ) → dom · = ( 𝐵 × 𝐵 ) )
14 13 releqd ⊢ ( · Fn ( 𝐵 × 𝐵 ) → ( Rel dom · ↔ Rel ( 𝐵 × 𝐵 ) ) )
15 12 14 mpbiri ⊢ ( · Fn ( 𝐵 × 𝐵 ) → Rel dom · )
16 tpostpos2 ⊢ ( ( Rel · ∧ Rel dom · ) → tpos tpos · = · )
17 11 15 16 syl2anc ⊢ ( · Fn ( 𝐵 × 𝐵 ) → tpos tpos · = · )
18 10 17 eqtrid ⊢ ( · Fn ( 𝐵 × 𝐵 ) → tpos ( .r ‘ 𝑂 ) = · )
19 6 18 syl ⊢ ( 𝜑 → tpos ( .r ‘ 𝑂 ) = · )
20 19 2 eqtrdi ⊢ ( 𝜑 → tpos ( .r ‘ 𝑂 ) = ( .r ‘ 𝑅 ) )
21 20 opeq2d ⊢ ( 𝜑 → ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ = ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
23 1 7 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
24 eqid ⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
25 23 8 24 opprval ⊢ ( oppr ‘ 𝑂 ) = ( 𝑂 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ )
26 7 2 1 opprval ⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
27 26 oveq1i ⊢ ( 𝑂 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) = ( ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ )
28 25 27 eqtri ⊢ ( oppr ‘ 𝑂 ) = ( ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ )
29 fvex ⊢ ( .r ‘ 𝑂 ) ∈ V
30 29 tposex ⊢ tpos ( .r ‘ 𝑂 ) ∈ V
31 setsabs ⊢ ( ( 𝑅 ∈ 𝑉 ∧ tpos ( .r ‘ 𝑂 ) ∈ V ) → ( ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) )
32 30 31 mpan2 ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) )
33 28 32 eqtrid ⊢ ( 𝑅 ∈ 𝑉 → ( oppr ‘ 𝑂 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) )
34 3 33 syl ⊢ ( 𝜑 → ( oppr ‘ 𝑂 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑂 ) ⟩ ) )
35 mulridx ⊢ .r = Slot ( .r ‘ ndx )
36 35 3 4 5 setsidvald ⊢ ( 𝜑 → 𝑅 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑅 ) ⟩ ) )
37 22 34 36 3eqtr4rd ⊢ ( 𝜑 → 𝑅 = ( oppr ‘ 𝑂 ) )