df-rngoiso - Mathbox for Jeff Madsen

	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 32945

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 (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})

Distinct variable group: 𝑠,𝑟,𝑓

**Detailed syntax breakdown of Definition df-rngoiso**
Step	Hyp	Ref	Expression
1		crngiso 32930	. 2 class RngIso
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 32863	. . 3 class RingOps
5	2	cv 1474	. . . . . . 7 class 𝑟
6		c1st 7057	. . . . . . 7 class 1^st
7	5, 6	cfv 5804	. . . . . 6 class (1^st ‘𝑟)
8	7	crn 5039	. . . . 5 class ran (1^st ‘𝑟)
9	3	cv 1474	. . . . . . 7 class 𝑠
10	9, 6	cfv 5804	. . . . . 6 class (1^st ‘𝑠)
11	10	crn 5039	. . . . 5 class ran (1^st ‘𝑠)
12		vf	. . . . . 6 setvar 𝑓
13	12	cv 1474	. . . . 5 class 𝑓
14	8, 11, 13	wf1o 5803	. . . 4 wff 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)
15		crnghom 32929	. . . . 5 class RngHom
16	5, 9, 15	co 6549	. . . 4 class (𝑟 RngHom 𝑠)
17	14, 12, 16	crab 2900	. . 3 class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)}
18	2, 3, 4, 4, 17	cmpt2 6551	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})
19	1, 18	wceq 1475	1 wff RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})

Colors of variables: wff setvar class

This definition is referenced by: rngoisoval 32946