MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rnghom Structured version   Visualization version   GIF version

Definition df-rnghom 18480
Description: Define the set of ring homomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
df-rnghom RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))})
Distinct variable group:   𝑠,𝑟,𝑣,𝑤,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-rnghom
StepHypRef Expression
1 crh 18477 . 2 class RingHom
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crg 18312 . . 3 class Ring
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 cur 18266 . . . . . . . . . 10 class 1r
136, 12cfv 5786 . . . . . . . . 9 class (1r𝑟)
14 vf . . . . . . . . . 10 setvar 𝑓
1514cv 1473 . . . . . . . . 9 class 𝑓
1613, 15cfv 5786 . . . . . . . 8 class (𝑓‘(1r𝑟))
1710, 12cfv 5786 . . . . . . . 8 class (1r𝑠)
1816, 17wceq 1474 . . . . . . 7 wff (𝑓‘(1r𝑟)) = (1r𝑠)
19 vx . . . . . . . . . . . . . 14 setvar 𝑥
2019cv 1473 . . . . . . . . . . . . 13 class 𝑥
21 vy . . . . . . . . . . . . . 14 setvar 𝑦
2221cv 1473 . . . . . . . . . . . . 13 class 𝑦
23 cplusg 15710 . . . . . . . . . . . . . 14 class +g
246, 23cfv 5786 . . . . . . . . . . . . 13 class (+g𝑟)
2520, 22, 24co 6523 . . . . . . . . . . . 12 class (𝑥(+g𝑟)𝑦)
2625, 15cfv 5786 . . . . . . . . . . 11 class (𝑓‘(𝑥(+g𝑟)𝑦))
2720, 15cfv 5786 . . . . . . . . . . . 12 class (𝑓𝑥)
2822, 15cfv 5786 . . . . . . . . . . . 12 class (𝑓𝑦)
2910, 23cfv 5786 . . . . . . . . . . . 12 class (+g𝑠)
3027, 28, 29co 6523 . . . . . . . . . . 11 class ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
3126, 30wceq 1474 . . . . . . . . . 10 wff (𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦))
32 cmulr 15711 . . . . . . . . . . . . . 14 class .r
336, 32cfv 5786 . . . . . . . . . . . . 13 class (.r𝑟)
3420, 22, 33co 6523 . . . . . . . . . . . 12 class (𝑥(.r𝑟)𝑦)
3534, 15cfv 5786 . . . . . . . . . . 11 class (𝑓‘(𝑥(.r𝑟)𝑦))
3610, 32cfv 5786 . . . . . . . . . . . 12 class (.r𝑠)
3727, 28, 36co 6523 . . . . . . . . . . 11 class ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3835, 37wceq 1474 . . . . . . . . . 10 wff (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))
3931, 38wa 382 . . . . . . . . 9 wff ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
405cv 1473 . . . . . . . . 9 class 𝑣
4139, 21, 40wral 2891 . . . . . . . 8 wff 𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
4241, 19, 40wral 2891 . . . . . . 7 wff 𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦)))
4318, 42wa 382 . . . . . 6 wff ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))
449cv 1473 . . . . . . 7 class 𝑤
45 cmap 7717 . . . . . . 7 class 𝑚
4644, 40, 45co 6523 . . . . . 6 class (𝑤𝑚 𝑣)
4743, 14, 46crab 2895 . . . . 5 class {𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))}
489, 11, 47csb 3494 . . . 4 class (Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))}
495, 8, 48csb 3494 . . 3 class (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))}
502, 3, 4, 4, 49cmpt2 6525 . 2 class (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))})
511, 50wceq 1474 1 wff RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ (Base‘𝑟) / 𝑣(Base‘𝑠) / 𝑤{𝑓 ∈ (𝑤𝑚 𝑣) ∣ ((𝑓‘(1r𝑟)) = (1r𝑠) ∧ ∀𝑥𝑣𝑦𝑣 ((𝑓‘(𝑥(+g𝑟)𝑦)) = ((𝑓𝑥)(+g𝑠)(𝑓𝑦)) ∧ (𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥)(.r𝑠)(𝑓𝑦))))})
Colors of variables: wff setvar class
This definition is referenced by:  dfrhm2  18482
  Copyright terms: Public domain W3C validator