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
|- O = ( oppR ` R )
opprabs.m
|- .x. = ( .r ` R )
opprabs.1
|- ( ph -> R e. V )
opprabs.2
|- ( ph -> Fun R )
opprabs.3
|- ( ph -> ( .r ` ndx ) e. dom R )
opprabs.4
|- ( ph -> .x. Fn ( B X. B ) )
Assertion opprabs
|- ( ph -> R = ( oppR ` O ) )

Proof

Step Hyp Ref Expression
1 opprabs.o
 |-  O = ( oppR ` R )
2 opprabs.m
 |-  .x. = ( .r ` R )
3 opprabs.1
 |-  ( ph -> R e. V )
4 opprabs.2
 |-  ( ph -> Fun R )
5 opprabs.3
 |-  ( ph -> ( .r ` ndx ) e. dom R )
6 opprabs.4
 |-  ( ph -> .x. Fn ( B X. B ) )
7 eqid
 |-  ( Base ` R ) = ( Base ` R )
8 eqid
 |-  ( .r ` O ) = ( .r ` O )
9 7 2 1 8 opprmulfval
 |-  ( .r ` O ) = tpos .x.
10 9 tposeqi
 |-  tpos ( .r ` O ) = tpos tpos .x.
11 fnrel
 |-  ( .x. Fn ( B X. B ) -> Rel .x. )
12 relxp
 |-  Rel ( B X. B )
13 fndm
 |-  ( .x. Fn ( B X. B ) -> dom .x. = ( B X. B ) )
14 13 releqd
 |-  ( .x. Fn ( B X. B ) -> ( Rel dom .x. <-> Rel ( B X. B ) ) )
15 12 14 mpbiri
 |-  ( .x. Fn ( B X. B ) -> Rel dom .x. )
16 tpostpos2
 |-  ( ( Rel .x. /\ Rel dom .x. ) -> tpos tpos .x. = .x. )
17 11 15 16 syl2anc
 |-  ( .x. Fn ( B X. B ) -> tpos tpos .x. = .x. )
18 10 17 eqtrid
 |-  ( .x. Fn ( B X. B ) -> tpos ( .r ` O ) = .x. )
19 6 18 syl
 |-  ( ph -> tpos ( .r ` O ) = .x. )
20 19 2 eqtrdi
 |-  ( ph -> tpos ( .r ` O ) = ( .r ` R ) )
21 20 opeq2d
 |-  ( ph -> <. ( .r ` ndx ) , tpos ( .r ` O ) >. = <. ( .r ` ndx ) , ( .r ` R ) >. )
22 21 oveq2d
 |-  ( ph -> ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) )
23 1 7 opprbas
 |-  ( Base ` R ) = ( Base ` O )
24 eqid
 |-  ( oppR ` O ) = ( oppR ` O )
25 23 8 24 opprval
 |-  ( oppR ` O ) = ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
26 7 2 1 opprval
 |-  O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )
27 26 oveq1i
 |-  ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
28 25 27 eqtri
 |-  ( oppR ` O ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
29 fvex
 |-  ( .r ` O ) e. _V
30 29 tposex
 |-  tpos ( .r ` O ) e. _V
31 setsabs
 |-  ( ( R e. V /\ tpos ( .r ` O ) e. _V ) -> ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
32 30 31 mpan2
 |-  ( R e. V -> ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
33 28 32 eqtrid
 |-  ( R e. V -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
34 3 33 syl
 |-  ( ph -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
35 mulridx
 |-  .r = Slot ( .r ` ndx )
36 35 3 4 5 setsidvald
 |-  ( ph -> R = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) )
37 22 34 36 3eqtr4rd
 |-  ( ph -> R = ( oppR ` O ) )