Users' Mathboxes 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 33755
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 33740 . 2 class RngIso
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 33673 . . 3 class RingOps
52cv 1481 . . . . . . 7 class 𝑟
6 c1st 7163 . . . . . . 7 class 1st
75, 6cfv 5886 . . . . . 6 class (1st𝑟)
87crn 5113 . . . . 5 class ran (1st𝑟)
93cv 1481 . . . . . . 7 class 𝑠
109, 6cfv 5886 . . . . . 6 class (1st𝑠)
1110crn 5113 . . . . 5 class ran (1st𝑠)
12 vf . . . . . 6 setvar 𝑓
1312cv 1481 . . . . 5 class 𝑓
148, 11, 13wf1o 5885 . . . 4 wff 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)
15 crnghom 33739 . . . . 5 class RngHom
165, 9, 15co 6647 . . . 4 class (𝑟 RngHom 𝑠)
1714, 12, 16crab 2915 . . 3 class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)}
182, 3, 4, 4, 17cmpt2 6649 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
191, 18wceq 1482 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  33756
  Copyright terms: Public domain W3C validator