Definition df-rnghomo 41677

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

Step	Hyp	Ref	Expression
1		crngh 41675	. 2 class RngHomo
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crng 41664	. . 3 class Rng
5		vv	. . . 4 setvar 𝑣
6	2	cv 1474	. . . . 5 class 𝑟
7		cbs 15695	. . . . 5 class Base
8	6, 7	cfv 5804	. . . 4 class (Base‘𝑟)
9		vw	. . . . 5 setvar 𝑤
10	3	cv 1474	. . . . . 6 class 𝑠
11	10, 7	cfv 5804	. . . . 5 class (Base‘𝑠)
12		vx	. . . . . . . . . . . . 13 setvar 𝑥
13	12	cv 1474	. . . . . . . . . . . 12 class 𝑥
14		vy	. . . . . . . . . . . . 13 setvar 𝑦
15	14	cv 1474	. . . . . . . . . . . 12 class 𝑦
16		cplusg 15768	. . . . . . . . . . . . 13 class +g
17	6, 16	cfv 5804	. . . . . . . . . . . 12 class (+g‘𝑟)
18	13, 15, 17	co 6549	. . . . . . . . . . 11 class (𝑥(+g‘𝑟)𝑦)
19		vf	. . . . . . . . . . . 12 setvar 𝑓
20	19	cv 1474	. . . . . . . . . . 11 class 𝑓
21	18, 20	cfv 5804	. . . . . . . . . 10 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
22	13, 20	cfv 5804	. . . . . . . . . . 11 class (𝑓‘𝑥)
23	15, 20	cfv 5804	. . . . . . . . . . 11 class (𝑓‘𝑦)
24	10, 16	cfv 5804	. . . . . . . . . . 11 class (+g‘𝑠)
25	22, 23, 24	co 6549	. . . . . . . . . 10 class ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
26	21, 25	wceq 1475	. . . . . . . . 9 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
27		cmulr 15769	. . . . . . . . . . . . 13 class .r
28	6, 27	cfv 5804	. . . . . . . . . . . 12 class (.r‘𝑟)
29	13, 15, 28	co 6549	. . . . . . . . . . 11 class (𝑥(.r‘𝑟)𝑦)
30	29, 20	cfv 5804	. . . . . . . . . 10 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
31	10, 27	cfv 5804	. . . . . . . . . . 11 class (.r‘𝑠)
32	22, 23, 31	co 6549	. . . . . . . . . 10 class ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
33	30, 32	wceq 1475	. . . . . . . . 9 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
34	26, 33	wa 383	. . . . . . . 8 wff ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
35	5	cv 1474	. . . . . . . 8 class 𝑣
36	34, 14, 35	wral 2896	. . . . . . 7 wff ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
37	36, 12, 35	wral 2896	. . . . . 6 wff ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
38	9	cv 1474	. . . . . . 7 class 𝑤
39		cmap 7744	. . . . . . 7 class ↑𝑚
40	38, 35, 39	co 6549	. . . . . 6 class (𝑤 ↑𝑚 𝑣)
41	37, 19, 40	crab 2900	. . . . 5 class {𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
42	9, 11, 41	csb 3499	. . . 4 class ⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
43	5, 8, 42	csb 3499	. . 3 class ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))}
44	2, 3, 4, 4, 43	cmpt2 6551	. 2 class (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})
45	1, 44	wceq 1475	1 wff RngHomo = (𝑟 ∈ Rng, 𝑠 ∈ Rng ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))})

This definition is referenced by:  rnghmrcl  41679  rnghmfn  41680  rnghmval  41681  rngchomrnghmresALTV  41788