Definition df-rngohom

Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Assertion	df-rngohom	$$⊢\mathrm{RngHom}=\left(r\in \mathrm{RingOps},s\in \mathrm{RingOps}⟼\left\{f\in \left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)|\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crnghom	$$class\mathrm{RngHom}$$
1		vr	$$setvarr$$
2		crngo	$$class\mathrm{RingOps}$$
3		vs	$$setvars$$
4		vf	$$setvarf$$
5		c1st	$$class{1}^{st}$$
6	3	cv	$$setvars$$
7	6 5	cfv	$$class{1}^{st}\left(s\right)$$
8	7	crn	$$class\mathrm{ran}{1}^{st}\left(s\right)$$
9		cmap	$$class{\uparrow }_{𝑚}$$
10	1	cv	$$setvarr$$
11	10 5	cfv	$$class{1}^{st}\left(r\right)$$
12	11	crn	$$class\mathrm{ran}{1}^{st}\left(r\right)$$
13	8 12 9	co	$$class\left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)$$
14	4	cv	$$setvarf$$
15		cgi	$$class\mathrm{GId}$$
16		c2nd	$$class{2}^{nd}$$
17	10 16	cfv	$$class{2}^{nd}\left(r\right)$$
18	17 15	cfv	$$class\mathrm{GId}\left(2^{nd}\left(r\right)\right)$$
19	18 14	cfv	$$classf\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)$$
20	6 16	cfv	$$class{2}^{nd}\left(s\right)$$
21	20 15	cfv	$$class\mathrm{GId}\left(2^{nd}\left(s\right)\right)$$
22	19 21	wceq	$$wfff\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)$$
23		vx	$$setvarx$$
24		vy	$$setvary$$
25	23	cv	$$setvarx$$
26	24	cv	$$setvary$$
27	25 26 11	co	$$class\left(x{1}^{st}\left(r\right)y\right)$$
28	27 14	cfv	$$classf\left(x{1}^{st}\left(r\right)y\right)$$
29	25 14	cfv	$$classf\left(x\right)$$
30	26 14	cfv	$$classf\left(y\right)$$
31	29 30 7	co	$$class\left(f\left(x\right)1^{st}\left(s\right)f\left(y\right)\right)$$
32	28 31	wceq	$$wfff\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)$$
33	25 26 17	co	$$class\left(x{2}^{nd}\left(r\right)y\right)$$
34	33 14	cfv	$$classf\left(x{2}^{nd}\left(r\right)y\right)$$
35	29 30 20	co	$$class\left(f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)$$
36	34 35	wceq	$$wfff\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)$$
37	32 36	wa	$$wff\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)$$
38	37 24 12	wral	$$wff\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)$$
39	38 23 12	wral	$$wff\forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)$$
40	22 39	wa	$$wff\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)$$
41	40 4 13	crab	$$class\left\{f\in \left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)|\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)\right\}$$
42	1 3 2 2 41	cmpo	$$class\left(r\in \mathrm{RingOps},s\in \mathrm{RingOps}⟼\left\{f\in \left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)|\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)\right\}\right)$$
43	0 42	wceq	$$wff\mathrm{RngHom}=\left(r\in \mathrm{RingOps},s\in \mathrm{RingOps}⟼\left\{f\in \left({\mathrm{ran}{1}^{st}\left(s\right)}^{\mathrm{ran}{1}^{st}\left(r\right)}\right)|\left(f\left(\mathrm{GId}\left(2^{nd}\left(r\right)\right)\right)=\mathrm{GId}\left(2^{nd}\left(s\right)\right)\wedge \forall x\in \mathrm{ran}{1}^{st}\left(r\right)\forall y\in \mathrm{ran}{1}^{st}\left(r\right)\left(f\left(x{1}^{st}\left(r\right)y\right)=f\left(x\right)1^{st}\left(s\right)f\left(y\right)\wedge f\left(x{2}^{nd}\left(r\right)y\right)=f\left(x\right)2^{nd}\left(s\right)f\left(y\right)\right)\right)\right\}\right)$$