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

Theorem riscer 34069
 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 34064 . . 3 𝑟 = {⟨𝑟, 𝑠⟩ ∣ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠))}
21relopabi 5389 . 2 Rel ≃𝑟
3 eqid 2748 . 2 dom ≃𝑟 = dom ≃𝑟
4 vex 3331 . . . . . . 7 𝑟 ∈ V
5 vex 3331 . . . . . . 7 𝑠 ∈ V
64, 5isrisc 34066 . . . . . 6 (𝑟𝑟 𝑠 ↔ ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)))
7 rngoisocnv 34062 . . . . . . . . . 10 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑓 ∈ (𝑟 RngIso 𝑠)) → 𝑓 ∈ (𝑠 RngIso 𝑟))
873expia 1114 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑟 RngIso 𝑠) → 𝑓 ∈ (𝑠 RngIso 𝑟)))
9 risci 34068 . . . . . . . . . . 11 ((𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps ∧ 𝑓 ∈ (𝑠 RngIso 𝑟)) → 𝑠𝑟 𝑟)
1093expia 1114 . . . . . . . . . 10 ((𝑠 ∈ RingOps ∧ 𝑟 ∈ RingOps) → (𝑓 ∈ (𝑠 RngIso 𝑟) → 𝑠𝑟 𝑟))
1110ancoms 468 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑠 RngIso 𝑟) → 𝑠𝑟 𝑟))
128, 11syld 47 . . . . . . . 8 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (𝑓 ∈ (𝑟 RngIso 𝑠) → 𝑠𝑟 𝑟))
1312exlimdv 1998 . . . . . . 7 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) → (∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) → 𝑠𝑟 𝑟))
1413imp 444 . . . . . 6 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)) → 𝑠𝑟 𝑟)
156, 14sylbi 207 . . . . 5 (𝑟𝑟 𝑠𝑠𝑟 𝑟)
16 vex 3331 . . . . . . 7 𝑡 ∈ V
175, 16isrisc 34066 . . . . . 6 (𝑠𝑟 𝑡 ↔ ((𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡)))
18 eeanv 2315 . . . . . . . . . . 11 (∃𝑓𝑔(𝑓 ∈ (𝑟 RngIso 𝑠) ∧ 𝑔 ∈ (𝑠 RngIso 𝑡)) ↔ (∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡)))
19 rngoisoco 34063 . . . . . . . . . . . . . 14 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ (𝑓 ∈ (𝑟 RngIso 𝑠) ∧ 𝑔 ∈ (𝑠 RngIso 𝑡))) → (𝑔𝑓) ∈ (𝑟 RngIso 𝑡))
2019ex 449 . . . . . . . . . . . . 13 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑓 ∈ (𝑟 RngIso 𝑠) ∧ 𝑔 ∈ (𝑠 RngIso 𝑡)) → (𝑔𝑓) ∈ (𝑟 RngIso 𝑡)))
21 risci 34068 . . . . . . . . . . . . . . 15 ((𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps ∧ (𝑔𝑓) ∈ (𝑟 RngIso 𝑡)) → 𝑟𝑟 𝑡)
22213expia 1114 . . . . . . . . . . . . . 14 ((𝑟 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑔𝑓) ∈ (𝑟 RngIso 𝑡) → 𝑟𝑟 𝑡))
23223adant2 1123 . . . . . . . . . . . . 13 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑔𝑓) ∈ (𝑟 RngIso 𝑡) → 𝑟𝑟 𝑡))
2420, 23syld 47 . . . . . . . . . . . 12 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((𝑓 ∈ (𝑟 RngIso 𝑠) ∧ 𝑔 ∈ (𝑠 RngIso 𝑡)) → 𝑟𝑟 𝑡))
2524exlimdvv 1999 . . . . . . . . . . 11 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → (∃𝑓𝑔(𝑓 ∈ (𝑟 RngIso 𝑠) ∧ 𝑔 ∈ (𝑠 RngIso 𝑡)) → 𝑟𝑟 𝑡))
2618, 25syl5bir 233 . . . . . . . . . 10 ((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) → ((∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡)) → 𝑟𝑟 𝑡))
27263expb 1113 . . . . . . . . 9 ((𝑟 ∈ RingOps ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) → ((∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡)) → 𝑟𝑟 𝑡))
2827adantlr 753 . . . . . . . 8 (((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) → ((∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡)) → 𝑟𝑟 𝑡))
2928imp 444 . . . . . . 7 ((((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ (𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps)) ∧ (∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡))) → 𝑟𝑟 𝑡)
3029an4s 904 . . . . . 6 ((((𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps) ∧ ∃𝑓 𝑓 ∈ (𝑟 RngIso 𝑠)) ∧ ((𝑠 ∈ RingOps ∧ 𝑡 ∈ RingOps) ∧ ∃𝑔 𝑔 ∈ (𝑠 RngIso 𝑡))) → 𝑟𝑟 𝑡)
316, 17, 30syl2anb 497 . . . . 5 ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡)
3215, 31pm3.2i 470 . . . 4 ((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
3332ax-gen 1859 . . 3 𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
3433gen2 1860 . 2 𝑟𝑠𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))
35 dfer2 7900 . 2 ( ≃𝑟 Er dom ≃𝑟 ↔ (Rel ≃𝑟 ∧ dom ≃𝑟 = dom ≃𝑟 ∧ ∀𝑟𝑠𝑡((𝑟𝑟 𝑠𝑠𝑟 𝑟) ∧ ((𝑟𝑟 𝑠𝑠𝑟 𝑡) → 𝑟𝑟 𝑡))))
362, 3, 34, 35mpbir3an 1405 1 𝑟 Er dom ≃𝑟
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072  ∀wal 1618   = wceq 1620  ∃wex 1841   ∈ wcel 2127   class class class wbr 4792  ◡ccnv 5253  dom cdm 5254   ∘ ccom 5258  Rel wrel 5259  (class class class)co 6801   Er wer 7896  RingOpscrngo 33975   RngIso crngiso 34042   ≃𝑟 crisc 34043 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-1st 7321  df-2nd 7322  df-er 7899  df-map 8013  df-grpo 27627  df-gid 27628  df-ablo 27679  df-ass 33924  df-exid 33926  df-mgmOLD 33930  df-sgrOLD 33942  df-mndo 33948  df-rngo 33976  df-rngohom 34044  df-rngoiso 34057  df-risc 34064 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator