Definition df-rhm 13708

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

Assertion

Ref	Expression
df-rhm	|- RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )

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

Detailed syntax breakdown of Definition df-rhm

Step	Hyp	Ref	Expression
1		crh 13706	. 2 class RingHom
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crg 13552	. . 3 class Ring
5		vv	. . . 4 setvar v
6	2	cv 1363	. . . . 5 class r
7		cbs 12678	. . . . 5 class Base
8	6, 7	cfv 5258	. . . 4 class ( Base ` r )
9		vw	. . . . 5 setvar w
10	3	cv 1363	. . . . . 6 class s
11	10, 7	cfv 5258	. . . . 5 class ( Base ` s )
12		cur 13515	. . . . . . . . . 10 class 1r
13	6, 12	cfv 5258	. . . . . . . . 9 class ( 1r ` r )
14		vf	. . . . . . . . . 10 setvar f
15	14	cv 1363	. . . . . . . . 9 class f
16	13, 15	cfv 5258	. . . . . . . 8 class ( f ` ( 1r ` r ) )
17	10, 12	cfv 5258	. . . . . . . 8 class ( 1r ` s )
18	16, 17	wceq 1364	. . . . . . 7 wff ( f ` ( 1r ` r ) ) = ( 1r ` s )
19		vx	. . . . . . . . . . . . . 14 setvar x
20	19	cv 1363	. . . . . . . . . . . . 13 class x
21		vy	. . . . . . . . . . . . . 14 setvar y
22	21	cv 1363	. . . . . . . . . . . . 13 class y
23		cplusg 12755	. . . . . . . . . . . . . 14 class +g
24	6, 23	cfv 5258	. . . . . . . . . . . . 13 class ( +g ` r )
25	20, 22, 24	co 5922	. . . . . . . . . . . 12 class ( x ( +g ` r ) y )
26	25, 15	cfv 5258	. . . . . . . . . . 11 class ( f ` ( x ( +g ` r ) y ) )
27	20, 15	cfv 5258	. . . . . . . . . . . 12 class ( f ` x )
28	22, 15	cfv 5258	. . . . . . . . . . . 12 class ( f ` y )
29	10, 23	cfv 5258	. . . . . . . . . . . 12 class ( +g ` s )
30	27, 28, 29	co 5922	. . . . . . . . . . 11 class ( ( f ` x ) ( +g ` s ) ( f ` y ) )
31	26, 30	wceq 1364	. . . . . . . . . 10 wff ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) )
32		cmulr 12756	. . . . . . . . . . . . . 14 class .r
33	6, 32	cfv 5258	. . . . . . . . . . . . 13 class ( .r ` r )
34	20, 22, 33	co 5922	. . . . . . . . . . . 12 class ( x ( .r ` r ) y )
35	34, 15	cfv 5258	. . . . . . . . . . 11 class ( f ` ( x ( .r ` r ) y ) )
36	10, 32	cfv 5258	. . . . . . . . . . . 12 class ( .r ` s )
37	27, 28, 36	co 5922	. . . . . . . . . . 11 class ( ( f ` x ) ( .r ` s ) ( f ` y ) )
38	35, 37	wceq 1364	. . . . . . . . . 10 wff ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) )
39	31, 38	wa 104	. . . . . . . . 9 wff ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
40	5	cv 1363	. . . . . . . . 9 class v
41	39, 21, 40	wral 2475	. . . . . . . 8 wff A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
42	41, 19, 40	wral 2475	. . . . . . 7 wff A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
43	18, 42	wa 104	. . . . . 6 wff ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) )
44	9	cv 1363	. . . . . . 7 class w
45		cmap 6707	. . . . . . 7 class ^m
46	44, 40, 45	co 5922	. . . . . 6 class ( w ^m v )
47	43, 14, 46	crab 2479	. . . . 5 class { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) }
48	9, 11, 47	csb 3084	. . . 4 class [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) }
49	5, 8, 48	csb 3084	. . 3 class [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) }
50	2, 3, 4, 4, 49	cmpo 5924	. 2 class ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )
51	1, 50	wceq 1364	1 wff RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )

This definition is referenced by:  dfrhm2  13710  rhmex  13713