Definition df-rnghm 20666

Description: Define the set of non-unital ring homomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)

Assertion

Ref	Expression
df-rnghm	⊢ RngHom = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})

Distinct variable group:   𝑠,𝑟,𝑣,𝑤,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-rnghm

Step	Hyp	Ref	Expression
1		crnghm 20664	. 2 class RngHom
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crng 20374	. . 3 class Rng
5		vv	. . . 4 setvar 𝑣
6	2	cv 1569	. . . . 5 class 𝑟
7		cbs 17387	. . . . 5 class Base
8	6, 7	cfv 6538	. . . 4 class (Base‘𝑟)
9		vw	. . . . 5 setvar 𝑤
10	3	cv 1569	. . . . . 6 class 𝑠
11	10, 7	cfv 6538	. . . . 5 class (Base‘𝑠)
12		vx	. . . . . . . . . . . . 13 setvar 𝑥
13	12	cv 1569	. . . . . . . . . . . 12 class 𝑥
14		vy	. . . . . . . . . . . . 13 setvar 𝑦
15	14	cv 1569	. . . . . . . . . . . 12 class 𝑦
16		cplusg 17428	. . . . . . . . . . . . 13 class +g
17	6, 16	cfv 6538	. . . . . . . . . . . 12 class (+g‘𝑟)
18	13, 15, 17	co 7420	. . . . . . . . . . 11 class (𝑥(+g‘𝑟)𝑦)
19		vf	. . . . . . . . . . . 12 setvar 𝑓
20	19	cv 1569	. . . . . . . . . . 11 class 𝑓
21	18, 20	cfv 6538	. . . . . . . . . 10 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
22	13, 20	cfv 6538	. . . . . . . . . . 11 class (𝑓‘𝑥)
23	15, 20	cfv 6538	. . . . . . . . . . 11 class (𝑓‘𝑦)
24	10, 16	cfv 6538	. . . . . . . . . . 11 class (+g‘𝑠)
25	22, 23, 24	co 7420	. . . . . . . . . 10 class ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
26	21, 25	wceq 1570	. . . . . . . . 9 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
27		cmulr 17429	. . . . . . . . . . . . 13 class .r
28	6, 27	cfv 6538	. . . . . . . . . . . 12 class (.r‘𝑟)
29	13, 15, 28	co 7420	. . . . . . . . . . 11 class (𝑥(.r‘𝑟)𝑦)
30	29, 20	cfv 6538	. . . . . . . . . 10 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
31	10, 27	cfv 6538	. . . . . . . . . . 11 class (.r‘𝑠)
32	22, 23, 31	co 7420	. . . . . . . . . 10 class ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
33	30, 32	wceq 1570	. . . . . . . . 9 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
34	26, 33	wa 401	. . . . . . . 8 wff ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
35	5	cv 1569	. . . . . . . 8 class 𝑣
36	34, 14, 35	wral 3077	. . . . . . 7 wff ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
37	36, 12, 35	wral 3077	. . . . . 6 wff ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
38	9	cv 1569	. . . . . . 7 class 𝑤
39		cmap 8847	. . . . . . 7 class ↑m
40	38, 35, 39	co 7420	. . . . . 6 class (𝑤 ↑m 𝑣)
41	37, 19, 40	crab 3413	. . . . 5 class {𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
42	9, 11, 41	csb 3847	. . . 4 class ⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
43	5, 8, 42	csb 3847	. . 3 class ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
44	2, 3, 4, 4, 43	cmpo 7422	. 2 class (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})
45	1, 44	wceq 1570	1 wff RngHom = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})

This definition is used by:  rnghmrcl  20668  rnghmfn  20669  rnghmval  20670  rngchomrnghmresALTV  49375