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 36438
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 36423 . 2 class RngIso
2 vr . . 3 setvar π‘Ÿ
3 vs . . 3 setvar 𝑠
4 crngo 36356 . . 3 class RingOps
52cv 1541 . . . . . . 7 class π‘Ÿ
6 c1st 7920 . . . . . . 7 class 1st
75, 6cfv 6497 . . . . . 6 class (1st β€˜π‘Ÿ)
87crn 5635 . . . . 5 class ran (1st β€˜π‘Ÿ)
93cv 1541 . . . . . . 7 class 𝑠
109, 6cfv 6497 . . . . . 6 class (1st β€˜π‘ )
1110crn 5635 . . . . 5 class ran (1st β€˜π‘ )
12 vf . . . . . 6 setvar 𝑓
1312cv 1541 . . . . 5 class 𝑓
148, 11, 13wf1o 6496 . . . 4 wff 𝑓:ran (1st β€˜π‘Ÿ)–1-1-ontoβ†’ran (1st β€˜π‘ )
15 crnghom 36422 . . . . 5 class RngHom
165, 9, 15co 7358 . . . 4 class (π‘Ÿ RngHom 𝑠)
1714, 12, 16crab 3408 . . 3 class {𝑓 ∈ (π‘Ÿ RngHom 𝑠) ∣ 𝑓:ran (1st β€˜π‘Ÿ)–1-1-ontoβ†’ran (1st β€˜π‘ )}
182, 3, 4, 4, 17cmpo 7360 . 2 class (π‘Ÿ ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (π‘Ÿ RngHom 𝑠) ∣ 𝑓:ran (1st β€˜π‘Ÿ)–1-1-ontoβ†’ran (1st β€˜π‘ )})
191, 18wceq 1542 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  36439
  Copyright terms: Public domain W3C validator