df-rngohom - Mathbox for Jeff Madsen

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

Definition df-rngohom 36048

Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)

**Assertion**
Ref	Expression
df-rngohom	⊢ RngHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1^st ‘𝑠) ↑_m ran (1^st ‘𝑟)) ∣ ((𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))))})

Distinct variable group: 𝑠,𝑟,𝑓,𝑥,𝑦

**Detailed syntax breakdown of Definition df-rngohom**
Step	Hyp	Ref	Expression
1		crnghom 36045	. 2 class RngHom
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 35979	. . 3 class RingOps
5	2	cv 1538	. . . . . . . . 9 class 𝑟
6		c2nd 7803	. . . . . . . . 9 class 2^nd
7	5, 6	cfv 6418	. . . . . . . 8 class (2^nd ‘𝑟)
8		cgi 28753	. . . . . . . 8 class GId
9	7, 8	cfv 6418	. . . . . . 7 class (GId‘(2^nd ‘𝑟))
10		vf	. . . . . . . 8 setvar 𝑓
11	10	cv 1538	. . . . . . 7 class 𝑓
12	9, 11	cfv 6418	. . . . . 6 class (𝑓‘(GId‘(2^nd ‘𝑟)))
13	3	cv 1538	. . . . . . . 8 class 𝑠
14	13, 6	cfv 6418	. . . . . . 7 class (2^nd ‘𝑠)
15	14, 8	cfv 6418	. . . . . 6 class (GId‘(2^nd ‘𝑠))
16	12, 15	wceq 1539	. . . . 5 wff (𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠))
17		vx	. . . . . . . . . . . 12 setvar 𝑥
18	17	cv 1538	. . . . . . . . . . 11 class 𝑥
19		vy	. . . . . . . . . . . 12 setvar 𝑦
20	19	cv 1538	. . . . . . . . . . 11 class 𝑦
21		c1st 7802	. . . . . . . . . . . 12 class 1^st
22	5, 21	cfv 6418	. . . . . . . . . . 11 class (1^st ‘𝑟)
23	18, 20, 22	co 7255	. . . . . . . . . 10 class (𝑥(1^st ‘𝑟)𝑦)
24	23, 11	cfv 6418	. . . . . . . . 9 class (𝑓‘(𝑥(1^st ‘𝑟)𝑦))
25	18, 11	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑥)
26	20, 11	cfv 6418	. . . . . . . . . 10 class (𝑓‘𝑦)
27	13, 21	cfv 6418	. . . . . . . . . 10 class (1^st ‘𝑠)
28	25, 26, 27	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦))
29	24, 28	wceq 1539	. . . . . . . 8 wff (𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦))
30	18, 20, 7	co 7255	. . . . . . . . . 10 class (𝑥(2^nd ‘𝑟)𝑦)
31	30, 11	cfv 6418	. . . . . . . . 9 class (𝑓‘(𝑥(2^nd ‘𝑟)𝑦))
32	25, 26, 14	co 7255	. . . . . . . . 9 class ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))
33	31, 32	wceq 1539	. . . . . . . 8 wff (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))
34	29, 33	wa 395	. . . . . . 7 wff ((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦)))
35	22	crn 5581	. . . . . . 7 class ran (1^st ‘𝑟)
36	34, 19, 35	wral 3063	. . . . . 6 wff ∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦)))
37	36, 17, 35	wral 3063	. . . . 5 wff ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦)))
38	16, 37	wa 395	. . . 4 wff ((𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))))
39	27	crn 5581	. . . . 5 class ran (1^st ‘𝑠)
40		cmap 8573	. . . . 5 class ↑_m
41	39, 35, 40	co 7255	. . . 4 class (ran (1^st ‘𝑠) ↑_m ran (1^st ‘𝑟))
42	38, 10, 41	crab 3067	. . 3 class {𝑓 ∈ (ran (1^st ‘𝑠) ↑_m ran (1^st ‘𝑟)) ∣ ((𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))))}
43	2, 3, 4, 4, 42	cmpo 7257	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1^st ‘𝑠) ↑_m ran (1^st ‘𝑟)) ∣ ((𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))))})
44	1, 43	wceq 1539	1 wff RngHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1^st ‘𝑠) ↑_m ran (1^st ‘𝑟)) ∣ ((𝑓‘(GId‘(2^nd ‘𝑟))) = (GId‘(2^nd ‘𝑠)) ∧ ∀𝑥 ∈ ran (1^st ‘𝑟)∀𝑦 ∈ ran (1^st ‘𝑟)((𝑓‘(𝑥(1^st ‘𝑟)𝑦)) = ((𝑓‘𝑥)(1^st ‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(2^nd ‘𝑟)𝑦)) = ((𝑓‘𝑥)(2^nd ‘𝑠)(𝑓‘𝑦))))})

Colors of variables: wff setvar class

This definition is referenced by: rngohomval 36049

W3C validator