Definition df-rhm

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

	Ref	Expression
Assertion	df-rhm	$$⊢\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crh	$$class\mathrm{RingHom}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7		vv	$$setvarv$$
8	3	cv	$$setvars$$
9	8 4	cfv	$$class{\mathrm{Base}}_s$$
10		vw	$$setvarw$$
11		vf	$$setvarf$$
12	10	cv	$$setvarw$$
13		cmap	$$class{\uparrow }_{𝑚}$$
14	7	cv	$$setvarv$$
15	12 14 13	co	$$class\left(w^v\right)$$
16	11	cv	$$setvarf$$
17		cur	$$class{1}_r$$
18	5 17	cfv	$$class{1}_r$$
19	18 16	cfv	$$classf\left(1_r\right)$$
20	8 17	cfv	$$class{1}_s$$
21	19 20	wceq	$$wfff\left(1_r\right)=1_s$$
22		vx	$$setvarx$$
23		vy	$$setvary$$
24	22	cv	$$setvarx$$
25		cplusg	$$class{+}_{𝑔}$$
26	5 25	cfv	$$class{+}_r$$
27	23	cv	$$setvary$$
28	24 27 26	co	$$class\left(x{+}_{r}y\right)$$
29	28 16	cfv	$$classf\left(x{+}_{r}y\right)$$
30	24 16	cfv	$$classf\left(x\right)$$
31	8 25	cfv	$$class{+}_s$$
32	27 16	cfv	$$classf\left(y\right)$$
33	30 32 31	co	$$class\left(f\left(x\right){+}_{s}f\left(y\right)\right)$$
34	29 33	wceq	$$wfff\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)$$
35		cmulr	$$class{\cdot }_{𝑟}$$
36	5 35	cfv	$$class{\cdot }_r$$
37	24 27 36	co	$$class\left(x{\cdot }_{r}y\right)$$
38	37 16	cfv	$$classf\left(x{\cdot }_{r}y\right)$$
39	8 35	cfv	$$class{\cdot }_s$$
40	30 32 39	co	$$class\left(f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
41	38 40	wceq	$$wfff\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)$$
42	34 41	wa	$$wff\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
43	42 23 14	wral	$$wff\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
44	43 22 14	wral	$$wff\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
45	21 44	wa	$$wff\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)$$
46	45 11 15	crab	$$class\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}$$
47	10 9 46	csb	$$class⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}$$
48	7 6 47	csb	$$class⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}$$
49	1 3 2 2 48	cmpo	$$class\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}\right)$$
50	0 49	wceq	$$wff\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}\right)$$