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 44450
 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‘𝑠) / 𝑤{𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
Distinct variable group:   𝑠,𝑟,𝑣,𝑤,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-rnghomo
StepHypRef Expression
1 crngh 44448 . 2 class RngHomo
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crng 44437 . . 3 class Rng
5 vv . . . 4 setvar 𝑣
62cv 1537 . . . . 5 class 𝑟
7 cbs 16474 . . . . 5 class Base
86, 7cfv 6334 . . . 4 class (Base‘𝑟)
9 vw . . . . 5 setvar 𝑤
103cv 1537 . . . . . 6 class 𝑠
1110, 7cfv 6334 . . . . 5 class (Base‘𝑠)
12 vx . . . . . . . . . . . . 13 setvar 𝑥
1312cv 1537 . . . . . . . . . . . 12 class 𝑥
14 vy . . . . . . . . . . . . 13 setvar 𝑦
1514cv 1537 . . . . . . . . . . . 12 class 𝑦
16 cplusg 16556 . . . . . . . . . . . . 13 class +g
176, 16cfv 6334 . . . . . . . . . . . 12 class (+g𝑟)
1813, 15, 17co 7140 . . . . . . . . . . 11 class (𝑥(+g𝑟)𝑦)
19 vf . . . . . . . . . . . 12 setvar 𝑓
2019cv 1537 . . . . . . . . . . 11 class 𝑓
2118, 20cfv 6334 . . . . . . . . . 10 class (𝑓‘(𝑥(+g𝑟)𝑦))
2213, 20cfv 6334 . . . . . . . . . . 11 class (𝑓𝑥)
2315, 20cfv 6334 . . . . . . . . . . 11 class (𝑓𝑦)
2410, 16cfv 6334 . . . . . . . . . . 11 class (+g𝑠)
2522, 23, 24co 7140 . . . . . . . . . 10 class ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
2621, 25wceq 1538 . . . . . . . . 9 wff (𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
27 cmulr 16557 . . . . . . . . . . . . 13 class .r
286, 27cfv 6334 . . . . . . . . . . . 12 class (.r𝑟)
2913, 15, 28co 7140 . . . . . . . . . . 11 class (𝑥(.r𝑟)𝑦)
3029, 20cfv 6334 . . . . . . . . . 10 class (𝑓‘(𝑥(.r𝑟)𝑦))
3110, 27cfv 6334 . . . . . . . . . . 11 class (.r𝑠)
3222, 23, 31co 7140 . . . . . . . . . 10 class ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3330, 32wceq 1538 . . . . . . . . 9 wff (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3426, 33wa 399 . . . . . . . 8 wff ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
355cv 1537 . . . . . . . 8 class 𝑣
3634, 14, 35wral 3130 . . . . . . 7 wff 𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
3736, 12, 35wral 3130 . . . . . 6 wff 𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
389cv 1537 . . . . . . 7 class 𝑤
39 cmap 8393 . . . . . . 7 class m
4038, 35, 39co 7140 . . . . . 6 class (𝑤m 𝑣)
4137, 19, 40crab 3134 . . . . 5 class {𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
429, 11, 41csb 3855 . . . 4 class (Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
435, 8, 42csb 3855 . . 3 class (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))}
442, 3, 4, 4, 43cmpo 7142 . 2 class (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
451, 44wceq 1538 1 wff RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤m 𝑣) ∣ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))})
 Colors of variables: wff setvar class This definition is referenced by:  rnghmrcl  44452  rnghmfn  44453  rnghmval  44454  rngchomrnghmresALTV  44559
 Copyright terms: Public domain W3C validator