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	Could not format assertion : No typesetting found for |- RingOpsHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngohom	Could not format RingOpsHom : No typesetting found for class RingOpsHom with typecode class
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	Could not format RingOpsHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } ) : No typesetting found for wff RingOpsHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } ) with typecode wff