Definition df-rngohom 33762

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

Assertion

Ref	Expression
df-rngohom	|- RngHom = ( 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 ) ) ) ) } )

Distinct variable group:   s, r, f, x, y

Detailed syntax breakdown of Definition df-rngohom

Step	Hyp	Ref	Expression
1		crnghom 33759	. 2 class RngHom
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crngo 33693	. . 3 class RingOps
5	2	cv 1482	. . . . . . . . 9 class r
6		c2nd 7167	. . . . . . . . 9 class 2nd
7	5, 6	cfv 5888	. . . . . . . 8 class ( 2nd ` r )
8		cgi 27344	. . . . . . . 8 class GId
9	7, 8	cfv 5888	. . . . . . 7 class (GId ` ( 2nd ` r ) )
10		vf	. . . . . . . 8 setvar f
11	10	cv 1482	. . . . . . 7 class f
12	9, 11	cfv 5888	. . . . . 6 class ( f ` (GId ` ( 2nd ` r ) ) )
13	3	cv 1482	. . . . . . . 8 class s
14	13, 6	cfv 5888	. . . . . . 7 class ( 2nd ` s )
15	14, 8	cfv 5888	. . . . . 6 class (GId ` ( 2nd ` s ) )
16	12, 15	wceq 1483	. . . . 5 wff ( f ` (GId ` ( 2nd ` r ) ) ) = (GId ` ( 2nd ` s ) )
17		vx	. . . . . . . . . . . 12 setvar x
18	17	cv 1482	. . . . . . . . . . 11 class x
19		vy	. . . . . . . . . . . 12 setvar y
20	19	cv 1482	. . . . . . . . . . 11 class y
21		c1st 7166	. . . . . . . . . . . 12 class 1st
22	5, 21	cfv 5888	. . . . . . . . . . 11 class ( 1st ` r )
23	18, 20, 22	co 6650	. . . . . . . . . 10 class ( x ( 1st ` r ) y )
24	23, 11	cfv 5888	. . . . . . . . 9 class ( f ` ( x ( 1st ` r ) y ) )
25	18, 11	cfv 5888	. . . . . . . . . 10 class ( f ` x )
26	20, 11	cfv 5888	. . . . . . . . . 10 class ( f ` y )
27	13, 21	cfv 5888	. . . . . . . . . 10 class ( 1st ` s )
28	25, 26, 27	co 6650	. . . . . . . . 9 class ( ( f ` x ) ( 1st ` s ) ( f ` y ) )
29	24, 28	wceq 1483	. . . . . . . 8 wff ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) )
30	18, 20, 7	co 6650	. . . . . . . . . 10 class ( x ( 2nd ` r ) y )
31	30, 11	cfv 5888	. . . . . . . . 9 class ( f ` ( x ( 2nd ` r ) y ) )
32	25, 26, 14	co 6650	. . . . . . . . 9 class ( ( f ` x ) ( 2nd ` s ) ( f ` y ) )
33	31, 32	wceq 1483	. . . . . . . 8 wff ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) )
34	29, 33	wa 384	. . . . . . 7 wff ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) )
35	22	crn 5115	. . . . . . 7 class ran ( 1st ` r )
36	34, 19, 35	wral 2912	. . . . . 6 wff 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 ) ) )
37	36, 17, 35	wral 2912	. . . . 5 wff 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 ) ) )
38	16, 37	wa 384	. . . 4 wff ( ( 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 ) ) ) )
39	27	crn 5115	. . . . 5 class ran ( 1st ` s )
40		cmap 7857	. . . . 5 class ^m
41	39, 35, 40	co 6650	. . . 4 class ( ran ( 1st ` s ) ^m ran ( 1st ` r ) )
42	38, 10, 41	crab 2916	. . 3 class { 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 ) ) ) ) }
43	2, 3, 4, 4, 42	cmpt2 6652	. 2 class ( 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 ) ) ) ) } )
44	1, 43	wceq 1483	1 wff RngHom = ( 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 ) ) ) ) } )

This definition is referenced by:  rngohomval  33763