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 33433
 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𝑠) ↑𝑚 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 33430 . 2 class RngHom
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 33364 . . 3 class RingOps
52cv 1479 . . . . . . . . 9 class 𝑟
6 c2nd 7127 . . . . . . . . 9 class 2nd
75, 6cfv 5857 . . . . . . . 8 class (2nd𝑟)
8 cgi 27232 . . . . . . . 8 class GId
97, 8cfv 5857 . . . . . . 7 class (GId‘(2nd𝑟))
10 vf . . . . . . . 8 setvar 𝑓
1110cv 1479 . . . . . . 7 class 𝑓
129, 11cfv 5857 . . . . . 6 class (𝑓‘(GId‘(2nd𝑟)))
133cv 1479 . . . . . . . 8 class 𝑠
1413, 6cfv 5857 . . . . . . 7 class (2nd𝑠)
1514, 8cfv 5857 . . . . . 6 class (GId‘(2nd𝑠))
1612, 15wceq 1480 . . . . 5 wff (𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠))
17 vx . . . . . . . . . . . 12 setvar 𝑥
1817cv 1479 . . . . . . . . . . 11 class 𝑥
19 vy . . . . . . . . . . . 12 setvar 𝑦
2019cv 1479 . . . . . . . . . . 11 class 𝑦
21 c1st 7126 . . . . . . . . . . . 12 class 1st
225, 21cfv 5857 . . . . . . . . . . 11 class (1st𝑟)
2318, 20, 22co 6615 . . . . . . . . . 10 class (𝑥(1st𝑟)𝑦)
2423, 11cfv 5857 . . . . . . . . 9 class (𝑓‘(𝑥(1st𝑟)𝑦))
2518, 11cfv 5857 . . . . . . . . . 10 class (𝑓𝑥)
2620, 11cfv 5857 . . . . . . . . . 10 class (𝑓𝑦)
2713, 21cfv 5857 . . . . . . . . . 10 class (1st𝑠)
2825, 26, 27co 6615 . . . . . . . . 9 class ((𝑓𝑥)(1st𝑠)(𝑓𝑦))
2924, 28wceq 1480 . . . . . . . 8 wff (𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦))
3018, 20, 7co 6615 . . . . . . . . . 10 class (𝑥(2nd𝑟)𝑦)
3130, 11cfv 5857 . . . . . . . . 9 class (𝑓‘(𝑥(2nd𝑟)𝑦))
3225, 26, 14co 6615 . . . . . . . . 9 class ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))
3331, 32wceq 1480 . . . . . . . 8 wff (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))
3429, 33wa 384 . . . . . . 7 wff ((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3522crn 5085 . . . . . . 7 class ran (1st𝑟)
3634, 19, 35wral 2908 . . . . . 6 wff 𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3736, 17, 35wral 2908 . . . . 5 wff 𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦)))
3816, 37wa 384 . . . 4 wff ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))
3927crn 5085 . . . . 5 class ran (1st𝑠)
40 cmap 7817 . . . . 5 class 𝑚
4139, 35, 40co 6615 . . . 4 class (ran (1st𝑠) ↑𝑚 ran (1st𝑟))
4238, 10, 41crab 2912 . . 3 class {𝑓 ∈ (ran (1st𝑠) ↑𝑚 ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))}
432, 3, 4, 4, 42cmpt2 6617 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st𝑠) ↑𝑚 ran (1st𝑟)) ∣ ((𝑓‘(GId‘(2nd𝑟))) = (GId‘(2nd𝑠)) ∧ ∀𝑥 ∈ ran (1st𝑟)∀𝑦 ∈ ran (1st𝑟)((𝑓‘(𝑥(1st𝑟)𝑦)) = ((𝑓𝑥)(1st𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(2nd𝑟)𝑦)) = ((𝑓𝑥)(2nd𝑠)(𝑓𝑦))))})
441, 43wceq 1480 1 wff RngHom = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (ran (1st𝑠) ↑𝑚 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  33434
 Copyright terms: Public domain W3C validator