Definition df-rnghomo

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

	Ref	Expression
Assertion	df-rnghomo	$$⊢\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngh	$$class\mathrm{RngHomo}$$
1		vr	$$setvarr$$
2		crng	$$class\mathrm{Rng}$$
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		vx	$$setvarx$$
17		vy	$$setvary$$
18	11	cv	$$setvarf$$
19	16	cv	$$setvarx$$
20		cplusg	$$class{+}_{𝑔}$$
21	5 20	cfv	$$class{+}_r$$
22	17	cv	$$setvary$$
23	19 22 21	co	$$class\left(x{+}_{r}y\right)$$
24	23 18	cfv	$$classf\left(x{+}_{r}y\right)$$
25	19 18	cfv	$$classf\left(x\right)$$
26	8 20	cfv	$$class{+}_s$$
27	22 18	cfv	$$classf\left(y\right)$$
28	25 27 26	co	$$class\left(f\left(x\right){+}_{s}f\left(y\right)\right)$$
29	24 28	wceq	$$wfff\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)$$
30		cmulr	$$class{\cdot }_{𝑟}$$
31	5 30	cfv	$$class{\cdot }_r$$
32	19 22 31	co	$$class\left(x{\cdot }_{r}y\right)$$
33	32 18	cfv	$$classf\left(x{\cdot }_{r}y\right)$$
34	8 30	cfv	$$class{\cdot }_s$$
35	25 27 34	co	$$class\left(f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
36	33 35	wceq	$$wfff\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)$$
37	29 36	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)$$
38	37 17 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)$$
39	38 16 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)$$
40	39 11 15	crab	$$class\left\{f\in \left(w^v\right)|\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\}$$
41	10 9 40	csb	$$class⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}$$
42	7 6 41	csb	$$class⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}$$
43	1 3 2 2 42	cmpo	$$class\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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)$$
44	0 43	wceq	$$wff\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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)$$