Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngonegmn1r Structured version   Unicode version

Theorem rngonegmn1r 28681
 Description: Negation in a ring is the same as right multiplication by . (Contributed by Jeff Madsen, 19-Jun-2010.)
Hypotheses
Ref Expression
ringneg.1
ringneg.2
ringneg.3
ringneg.4
ringneg.5 GId
Assertion
Ref Expression
rngonegmn1r

Proof of Theorem rngonegmn1r
StepHypRef Expression
1 ringneg.3 . . . . . . . . 9
2 ringneg.1 . . . . . . . . . 10
32rneqi 5062 . . . . . . . . 9
41, 3eqtri 2461 . . . . . . . 8
5 ringneg.2 . . . . . . . 8
6 ringneg.5 . . . . . . . 8 GId
74, 5, 6rngo1cl 23851 . . . . . . 7
8 ringneg.4 . . . . . . . 8
92, 1, 8rngonegcl 28676 . . . . . . 7
107, 9mpdan 663 . . . . . 6
1110adantr 462 . . . . 5
127adantr 462 . . . . 5
1311, 12jca 529 . . . 4
142, 5, 1rngodi 23807 . . . . . 6
15143exp2 1200 . . . . 5
1615imp43 592 . . . 4
1713, 16mpdan 663 . . 3
18 eqid 2441 . . . . . . . 8 GId GId
192, 1, 8, 18rngoaddneg2 28678 . . . . . . 7 GId
207, 19mpdan 663 . . . . . 6 GId
2120adantr 462 . . . . 5 GId
2221oveq2d 6106 . . . 4 GId
2318, 1, 2, 5rngorz 23824 . . . 4 GId GId
2422, 23eqtrd 2473 . . 3 GId
255, 4, 6rngoridm 23847 . . . 4
2625oveq2d 6106 . . 3
2717, 24, 263eqtr3rd 2482 . 2 GId
282, 5, 1rngocl 23804 . . . 4
2911, 28mpd3an3 1310 . . 3
302rngogrpo 23812 . . . 4
311, 18, 8grpoinvid2 23653 . . . 4 GId
3230, 31syl3an1 1246 . . 3 GId
3329, 32mpd3an3 1310 . 2 GId
3427, 33mpbird 232 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1364   wcel 1761   crn 4837  cfv 5415  (class class class)co 6090  c1st 6574  c2nd 6575  cgr 23608  GIdcgi 23609  cgn 23610  crngo 23797 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-1st 6576  df-2nd 6577  df-grpo 23613  df-gid 23614  df-ginv 23615  df-ablo 23704  df-ass 23735  df-exid 23737  df-mgm 23741  df-sgr 23753  df-mndo 23760  df-rngo 23798 This theorem is referenced by:  rngonegrmul  28683
 Copyright terms: Public domain W3C validator