Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rnghomo Structured version   Visualization version   GIF version

Definition df-rnghomo 41675
Description: Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
Assertion
Ref Expression
df-rnghomo RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
Distinct variable group:   𝑠,𝑟,𝑣,𝑤,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-rnghomo
StepHypRef Expression
1 crngh 41673 . 2 class RngHomo
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crng 41662 . . 3 class Rng
5 vv . . . 4 setvar 𝑣
62cv 1473 . . . . 5 class 𝑟
7 cbs 15637 . . . . 5 class Base
86, 7cfv 5786 . . . 4 class (Base‘𝑟)
9 vw . . . . 5 setvar 𝑤
103cv 1473 . . . . . 6 class 𝑠
1110, 7cfv 5786 . . . . 5 class (Base‘𝑠)
12 vx . . . . . . . . . . . . 13 setvar 𝑥
1312cv 1473 . . . . . . . . . . . 12 class 𝑥
14 vy . . . . . . . . . . . . 13 setvar 𝑦
1514cv 1473 . . . . . . . . . . . 12 class 𝑦
16 cplusg 15710 . . . . . . . . . . . . 13 class +g
176, 16cfv 5786 . . . . . . . . . . . 12 class (+g𝑟)
1813, 15, 17co 6523 . . . . . . . . . . 11 class (𝑥(+g𝑟)𝑦)
19 vf . . . . . . . . . . . 12 setvar 𝑓
2019cv 1473 . . . . . . . . . . 11 class 𝑓
2118, 20cfv 5786 . . . . . . . . . 10 class (𝑓‘(𝑥(+g𝑟)𝑦))
2213, 20cfv 5786 . . . . . . . . . . 11 class (𝑓𝑥)
2315, 20cfv 5786 . . . . . . . . . . 11 class (𝑓𝑦)
2410, 16cfv 5786 . . . . . . . . . . 11 class (+g𝑠)
2522, 23, 24co 6523 . . . . . . . . . 10 class ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
2621, 25wceq 1474 . . . . . . . . 9 wff (𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
27 cmulr 15711 . . . . . . . . . . . . 13 class .r
286, 27cfv 5786 . . . . . . . . . . . 12 class (.r𝑟)
2913, 15, 28co 6523 . . . . . . . . . . 11 class (𝑥(.r𝑟)𝑦)
3029, 20cfv 5786 . . . . . . . . . 10 class (𝑓‘(𝑥(.r𝑟)𝑦))
3110, 27cfv 5786 . . . . . . . . . . 11 class (.r𝑠)
3222, 23, 31co 6523 . . . . . . . . . 10 class ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3330, 32wceq 1474 . . . . . . . . 9 wff (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3426, 33wa 382 . . . . . . . 8 wff ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
355cv 1473 . . . . . . . 8 class 𝑣
3634, 14, 35wral 2891 . . . . . . 7 wff 𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
3736, 12, 35wral 2891 . . . . . 6 wff 𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
389cv 1473 . . . . . . 7 class 𝑤
39 cmap 7717 . . . . . . 7 class 𝑚
4038, 35, 39co 6523 . . . . . 6 class (𝑤𝑚 𝑣)
4137, 19, 40crab 2895 . . . . 5 class {𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
429, 11, 41csb 3494 . . . 4 class (Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
435, 8, 42csb 3494 . . 3 class (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
442, 3, 4, 4, 43cmpt2 6525 . 2 class (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
451, 44wceq 1474 1 wff RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  rnghmrcl  41677  rnghmfn  41678  rnghmval  41679  rngchomrnghmresALTV  41786
  Copyright terms: Public domain W3C validator