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