Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  riscer Structured version   Visualization version   GIF version

Theorem riscer 37159
Description: Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.)
Assertion
Ref Expression
riscer 𝑟 Er dom ≃𝑟

Proof of Theorem riscer
Dummy variables 𝑓 𝑔 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-risc 37154 . . 3 𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠))}
21relopabiv 5820 . 2 Rel ≃𝑟
3 eqid 2732 . 2 dom ≃𝑟 = dom ≃𝑟
4 vex 3478 . . . . . . 7 𝑟 ∈ V
5 vex 3478 . . . . . . 7 𝑠 ∈ V
64, 5isrisc 37156 . . . . . 6 (𝑟𝑟 𝑠 ↔ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠)))
7 rngoisocnv 37152 . . . . . . . . . 10 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑓 ∈ (𝑟 RingOpsIso 𝑠)) → 𝑓 ∈ (𝑠 RingOpsIso 𝑟))
873expia 1121 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑟 RingOpsIso 𝑠) → 𝑓 ∈ (𝑠 RingOpsIso 𝑟)))
9 risci 37158 . . . . . . . . . . 11 ((𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps ∧ 𝑓 ∈ (𝑠 RingOpsIso 𝑟)) → 𝑠𝑟 𝑟)
1093expia 1121 . . . . . . . . . 10 ((𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps) → (𝑓 ∈ (𝑠 RingOpsIso 𝑟) → 𝑠𝑟 𝑟))
1110ancoms 459 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑠 RingOpsIso 𝑟) → 𝑠𝑟 𝑟))
128, 11syld 47 . . . . . . . 8 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑟 RingOpsIso 𝑠) → 𝑠𝑟 𝑟))
1312exlimdv 1936 . . . . . . 7 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) → 𝑠𝑟 𝑟))
1413imp 407 . . . . . 6 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠)) → 𝑠𝑟 𝑟)
156, 14sylbi 216 . . . . 5 (𝑟𝑟 𝑠𝑠𝑟 𝑟)
16 vex 3478 . . . . . . 7 𝑡 ∈ V
175, 16isrisc 37156 . . . . . 6 (𝑠𝑟 𝑡 ↔ ((𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡)))
18 exdistrv 1959 . . . . . . . . . . 11 (∃𝑓𝑔(𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) ↔ (∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡)))
19 rngoisoco 37153 . . . . . . . . . . . . . 14 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ (𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ 𝑔 ∈ (𝑠 RingOpsIso 𝑡))) → (𝑔𝑓) ∈ (𝑟 RingOpsIso 𝑡))
2019ex 413 . . . . . . . . . . . . 13 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → (𝑔𝑓) ∈ (𝑟 RingOpsIso 𝑡)))
21 risci 37158 . . . . . . . . . . . . . . 15 ((𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps ∧ (𝑔𝑓) ∈ (𝑟 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡)
22213expia 1121 . . . . . . . . . . . . . 14 ((𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑔𝑓) ∈ (𝑟 RingOpsIso 𝑡) → 𝑟𝑟 𝑡))
23223adant2 1131 . . . . . . . . . . . . 13 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑔𝑓) ∈ (𝑟 RingOpsIso 𝑡) → 𝑟𝑟 𝑡))
2420, 23syld 47 . . . . . . . . . . . 12 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡))
2524exlimdvv 1937 . . . . . . . . . . 11 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → (∃𝑓𝑔(𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡))
2618, 25biimtrrid 242 . . . . . . . . . 10 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡))
27263expb 1120 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) → ((∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡))
2827adantlr 713 . . . . . . . 8 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) → ((∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡)) → 𝑟𝑟 𝑡))
2928imp 407 . . . . . . 7 ((((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) ∧ (∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡))) → 𝑟𝑟 𝑡)
3029an4s 658 . . . . . 6 ((((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RingOpsIso 𝑠)) ∧ ((𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ ∃𝑔 𝑔 ∈ (𝑠 RingOpsIso 𝑡))) → 𝑟𝑟 𝑡)
316, 17, 30syl2anb 598 . . . . 5 ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡)
3215, 31pm3.2i 471 . . . 4 ((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
3332ax-gen 1797 . . 3 𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
3433gen2 1798 . 2 𝑟𝑠𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
35 dfer2 8706 . 2 ( ≃𝑟 Er dom ≃𝑟 ↔ (Rel ≃𝑟 ∧ dom ≃𝑟 = dom ≃𝑟 ∧ ∀𝑟𝑠𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))))
362, 3, 34, 35mpbir3an 1341 1 𝑟 Er dom ≃𝑟
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106   class class class wbr 5148  ccnv 5675  dom cdm 5676  ccom 5680  Rel wrel 5681  (class class class)co 7411   Er wer 8702  RingOpscrngo 37065   RingOpsIso crngoiso 37132  𝑟 crisc 37133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-er 8705  df-map 8824  df-grpo 30001  df-gid 30002  df-ablo 30053  df-ass 37014  df-exid 37016  df-mgmOLD 37020  df-sgrOLD 37032  df-mndo 37038  df-rngo 37066  df-rngohom 37134  df-rngoiso 37147  df-risc 37154
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator