Definition df-rhm 20472

Description: Define the set of ring homomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Assertion

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

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

Detailed syntax breakdown of Definition df-rhm

Step	Hyp	Ref	Expression
1		crh 20469	. 2 class RingHom
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crg 20230	. . 3 class Ring
5		vv	. . . 4 setvar 𝑣
6	2	cv 1539	. . . . 5 class 𝑟
7		cbs 17247	. . . . 5 class Base
8	6, 7	cfv 6561	. . . 4 class (Base‘𝑟)
9		vw	. . . . 5 setvar 𝑤
10	3	cv 1539	. . . . . 6 class 𝑠
11	10, 7	cfv 6561	. . . . 5 class (Base‘𝑠)
12		cur 20178	. . . . . . . . . 10 class 1r
13	6, 12	cfv 6561	. . . . . . . . 9 class (1r‘𝑟)
14		vf	. . . . . . . . . 10 setvar 𝑓
15	14	cv 1539	. . . . . . . . 9 class 𝑓
16	13, 15	cfv 6561	. . . . . . . 8 class (𝑓‘(1r‘𝑟))
17	10, 12	cfv 6561	. . . . . . . 8 class (1r‘𝑠)
18	16, 17	wceq 1540	. . . . . . 7 wff (𝑓‘(1r‘𝑟)) = (1r‘𝑠)
19		vx	. . . . . . . . . . . . . 14 setvar 𝑥
20	19	cv 1539	. . . . . . . . . . . . 13 class 𝑥
21		vy	. . . . . . . . . . . . . 14 setvar 𝑦
22	21	cv 1539	. . . . . . . . . . . . 13 class 𝑦
23		cplusg 17297	. . . . . . . . . . . . . 14 class +g
24	6, 23	cfv 6561	. . . . . . . . . . . . 13 class (+g‘𝑟)
25	20, 22, 24	co 7431	. . . . . . . . . . . 12 class (𝑥(+g‘𝑟)𝑦)
26	25, 15	cfv 6561	. . . . . . . . . . 11 class (𝑓‘(𝑥(+g‘𝑟)𝑦))
27	20, 15	cfv 6561	. . . . . . . . . . . 12 class (𝑓‘𝑥)
28	22, 15	cfv 6561	. . . . . . . . . . . 12 class (𝑓‘𝑦)
29	10, 23	cfv 6561	. . . . . . . . . . . 12 class (+g‘𝑠)
30	27, 28, 29	co 7431	. . . . . . . . . . 11 class ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
31	26, 30	wceq 1540	. . . . . . . . . 10 wff (𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))
32		cmulr 17298	. . . . . . . . . . . . . 14 class .r
33	6, 32	cfv 6561	. . . . . . . . . . . . 13 class (.r‘𝑟)
34	20, 22, 33	co 7431	. . . . . . . . . . . 12 class (𝑥(.r‘𝑟)𝑦)
35	34, 15	cfv 6561	. . . . . . . . . . 11 class (𝑓‘(𝑥(.r‘𝑟)𝑦))
36	10, 32	cfv 6561	. . . . . . . . . . . 12 class (.r‘𝑠)
37	27, 28, 36	co 7431	. . . . . . . . . . 11 class ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
38	35, 37	wceq 1540	. . . . . . . . . 10 wff (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))
39	31, 38	wa 395	. . . . . . . . 9 wff ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
40	5	cv 1539	. . . . . . . . 9 class 𝑣
41	39, 21, 40	wral 3061	. . . . . . . 8 wff ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
42	41, 19, 40	wral 3061	. . . . . . 7 wff ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))
43	18, 42	wa 395	. . . . . 6 wff ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))
44	9	cv 1539	. . . . . . 7 class 𝑤
45		cmap 8866	. . . . . . 7 class ↑m
46	44, 40, 45	co 7431	. . . . . 6 class (𝑤 ↑m 𝑣)
47	43, 14, 46	crab 3436	. . . . 5 class {𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}
48	9, 11, 47	csb 3899	. . . 4 class ⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}
49	5, 8, 48	csb 3899	. . 3 class ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}
50	2, 3, 4, 4, 49	cmpo 7433	. 2 class (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
51	1, 50	wceq 1540	1 wff RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑m 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})

This definition is referenced by:  dfrhm2  20474