opprabs.mmp

opprabs.mmp

$theorem opprabs

* The opposite ring of the opposite ring is the original ring.

h1::opprabs.o              |- O = ( oppR ` R )
h2::opprabs.m              |- .x. = ( .r ` R )
h3::opprabs.1        |- ( ph -> R e. V )
hd12::opprabs.2      |- ( ph -> Fun R )
hd13::opprabs.3      |- ( ph -> ( .r ` ndx ) e. dom R )
h4::opprabs.4           |- ( ph -> .x. Fn ( B X. B ) )
d1::eqid                   |- ( Base ` R ) = ( Base ` R )
10:d1,2,1:opprval       |- O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )
d3:1,d1:opprbas         |- ( Base ` R ) = ( Base ` O )
d4::eqid                   |- ( .r ` O ) = ( .r ` O )
d5::eqid                |- ( oppR ` O ) = ( oppR ` O )
20:d3,d4,d5:opprval
                       |- ( oppR ` O ) = ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
30:10:oveq1i           |- ( O sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
40:20,30:eqtri        |- ( oppR ` O ) = ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. )
d6::fvex                |- ( .r ` O ) e. _V
45:d6:tposex           |- tpos ( .r ` O ) e. _V
50::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 ) >. ) )
65:45,50:mpan2        |- ( R e. V -> ( ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
70:40,65:eqtrid      |- ( R e. V -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
80:d1,2,1,d4:opprmulfval
                          |- ( .r ` O ) = tpos .x.
85:80:tposeqi            |- tpos ( .r ` O ) = tpos tpos .x.
90::tpostpos2             |- ( ( Rel .x. /\ Rel dom .x. ) -> tpos tpos .x. = .x. )
95::fnrel                 |- ( .x. Fn ( B X. B ) -> Rel .x. )
100::fndm                   |- ( .x. Fn ( B X. B ) -> dom .x. = ( B X. B ) )
110:100:releqd             |- ( .x. Fn ( B X. B ) -> ( Rel dom .x. <-> Rel ( B X. B ) ) )
120::relxp                 |- Rel ( B X. B )
130:120,110:mpbiri        |- ( .x. Fn ( B X. B ) -> Rel dom .x. )
140:95,130,90:syl2anc
                         |- ( .x. Fn ( B X. B ) -> tpos tpos .x. = .x. )
150:85,140:eqtrid       |- ( .x. Fn ( B X. B ) -> tpos ( .r ` O ) = .x. )
160:4,150:syl          |- ( ph -> tpos ( .r ` O ) = .x. )
170:3,70:syl        |- ( ph -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) )
180:160:opeq2d       |- ( ph -> <. ( .r ` ndx ) , tpos ( .r ` O ) >. = <. ( .r ` ndx ) , .x. >. )
190:180:oveq2d      |- ( ph -> ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , .x. >. ) )
191:170,190:eqtrd  |- ( ph -> ( oppR ` O ) = ( R sSet <. ( .r ` ndx ) , .x. >. ) )
d10::mulridx         |- .r = Slot ( .r ` ndx )
198:d10,3,d12,d13:setsidvald
                    |- ( ph -> R = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) )
d15:160,2:eqtrdi      |- ( ph -> tpos ( .r ` O ) = ( .r ` R ) )
d14:d15:opeq2d       |- ( ph -> <. ( .r ` ndx ) , tpos ( .r ` O ) >. = <. ( .r ` ndx ) , ( .r ` R ) >. )
200:d14:oveq2d      |- ( ph -> ( R sSet <. ( .r ` ndx ) , tpos ( .r ` O ) >. ) = ( R sSet <. ( .r ` ndx ) , ( .r ` R ) >. ) )
qed:200,170,198:3eqtr4rd
                   |- ( ph -> R = ( oppR ` O ) )

$= ( cmulr cfv ctpos cop csts co wceq eqid cnx cxp wfn opprmulfval tposeqi wrel
   coppr cbs cdm fnrel relxp fndm releqd mpbiri tpostpos2 syl2anc eqtrid eqtrdi
   syl opeq2d oveq2d wcel opprbas opprval oveq1i eqtri cvv tposex setsabs mpan2
   fvex mulridx setsidvald 3eqtr4rd ) ACUAMNZEMNZOZPZQRZCVOCMNZPZQREUGNZCAVRWAC
   QAVQVTVOAVQDVTADBBUBZUCZVQDSLWDVQDOZOZDVPWECUHNZCVPDEWGTZHGVPTZUDUEWDDUFDUIZ
   UFZWFDSWCDUJWDWKWCUFBBUKWDWJWCWCDULUMUNDUOUPUQUSHURUTVAACFVBZWBVSSIWLWBCVOWE
   PQRZVRQRZVSWBEVRQRWNWGEVPWBWGCEGWHVCWIWBTVDEWMVRQWGCDEWHHGVDVEVFWLVQVGVBWNVS
   SVPEMVKVHVOWEVQCFVGVIVJUQUSACMVOFVLIJKVMVN $.