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 35277
 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 (1st𝑠) ↑m ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))})
Distinct variable group:   𝑠,𝑟,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-rngohom
StepHypRef Expression
1 crnghom 35274 . 2 class RngHom
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 35208 . . 3 class RingOps
52cv 1536 . . . . . . . . 9 class 𝑟
6 c2nd 7666 . . . . . . . . 9 class 2nd
75, 6cfv 6331 . . . . . . . 8 class (2nd𝑟)
8 cgi 28252 . . . . . . . 8 class GId
97, 8cfv 6331 . . . . . . 7 class (GId‘(2nd𝑟))
10 vf . . . . . . . 8 setvar 𝑓
1110cv 1536 . . . . . . 7 class 𝑓
129, 11cfv 6331 . . . . . 6 class (𝑓‘(GId‘(2nd𝑟)))
133cv 1536 . . . . . . . 8 class 𝑠
1413, 6cfv 6331 . . . . . . 7 class (2nd𝑠)
1514, 8cfv 6331 . . . . . 6 class (GId‘(2nd𝑠))
1612, 15wceq 1537 . . . . 5 wff (𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠))
17 vx . . . . . . . . . . . 12 setvar 𝑥
1817cv 1536 . . . . . . . . . . 11 class 𝑥
19 vy . . . . . . . . . . . 12 setvar 𝑦
2019cv 1536 . . . . . . . . . . 11 class 𝑦
21 c1st 7665 . . . . . . . . . . . 12 class 1st
225, 21cfv 6331 . . . . . . . . . . 11 class (1st𝑟)
2318, 20, 22co 7133 . . . . . . . . . 10 class (𝑥(1st𝑟)𝑦)
2423, 11cfv 6331 . . . . . . . . 9 class (𝑓‘(𝑥(1st𝑟)𝑦))
2518, 11cfv 6331 . . . . . . . . . 10 class (𝑓𝑥)
2620, 11cfv 6331 . . . . . . . . . 10 class (𝑓𝑦)
2713, 21cfv 6331 . . . . . . . . . 10 class (1st𝑠)
2825, 26, 27co 7133 . . . . . . . . 9 class ((𝑓𝑥)(1st𝑠)(𝑓𝑦))
2924, 28wceq 1537 . . . . . . . 8 wff (𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦))
3018, 20, 7co 7133 . . . . . . . . . 10 class (𝑥(2nd𝑟)𝑦)
3130, 11cfv 6331 . . . . . . . . 9 class (𝑓‘(𝑥(2nd𝑟)𝑦))
3225, 26, 14co 7133 . . . . . . . . 9 class ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))
3331, 32wceq 1537 . . . . . . . 8 wff (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))
3429, 33wa 398 . . . . . . 7 wff ((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3522crn 5532 . . . . . . 7 class ran (1st𝑟)
3634, 19, 35wral 3125 . . . . . 6 wff 𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3736, 17, 35wral 3125 . . . . 5 wff 𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3816, 37wa 398 . . . 4 wff ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))
3927crn 5532 . . . . 5 class ran (1st𝑠)
40 cmap 8384 . . . . 5 class m
4139, 35, 40co 7133 . . . 4 class (ran (1st𝑠) ↑m ran (1st𝑟))
4238, 10, 41crab 3129 . . 3 class {𝑓 ∈ (ran (1st𝑠) ↑m ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))}
432, 3, 4, 4, 42cmpo 7135 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st𝑠) ↑m ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))})
441, 43wceq 1537 1 wff RngHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st𝑠) ↑m ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))})
 Colors of variables: wff setvar class This definition is referenced by:  rngohomval  35278
 Copyright terms: Public domain W3C validator