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

Definition df-rngoiso 35407
 Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
df-rngoiso RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-rngoiso
StepHypRef Expression
1 crngiso 35392 . 2 class RngIso
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 35325 . . 3 class RingOps
52cv 1537 . . . . . . 7 class 𝑟
6 c1st 7673 . . . . . . 7 class 1st
75, 6cfv 6328 . . . . . 6 class (1st𝑟)
87crn 5524 . . . . 5 class ran (1st𝑟)
93cv 1537 . . . . . . 7 class 𝑠
109, 6cfv 6328 . . . . . 6 class (1st𝑠)
1110crn 5524 . . . . 5 class ran (1st𝑠)
12 vf . . . . . 6 setvar 𝑓
1312cv 1537 . . . . 5 class 𝑓
148, 11, 13wf1o 6327 . . . 4 wff 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)
15 crnghom 35391 . . . . 5 class RngHom
165, 9, 15co 7139 . . . 4 class (𝑟 RngHom 𝑠)
1714, 12, 16crab 3113 . . 3 class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)}
182, 3, 4, 4, 17cmpo 7141 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
191, 18wceq 1538 1 wff RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
 Colors of variables: wff setvar class This definition is referenced by:  rngoisoval  35408
 Copyright terms: Public domain W3C validator