Definition df-rnghom 13321

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

Assertion

Ref	Expression
df-rnghom	|- 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-rnghom

Step	Hyp	Ref	Expression
1		crh 13319	. 2 class RingHom
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crg 13179	. . 3 class Ring
5		vv	. . . 4 setvar v
6	2	cv 1352	. . . . 5 class r
7		cbs 12462	. . . . 5 class Base
8	6, 7	cfv 5217	. . . 4 class ( Base ` r )
9		vw	. . . . 5 setvar w
10	3	cv 1352	. . . . . 6 class s
11	10, 7	cfv 5217	. . . . 5 class ( Base ` s )
12		cur 13142	. . . . . . . . . 10 class 1r
13	6, 12	cfv 5217	. . . . . . . . 9 class ( 1r ` r )
14		vf	. . . . . . . . . 10 setvar f
15	14	cv 1352	. . . . . . . . 9 class f
16	13, 15	cfv 5217	. . . . . . . 8 class ( f ` ( 1r ` r ) )
17	10, 12	cfv 5217	. . . . . . . 8 class ( 1r ` s )
18	16, 17	wceq 1353	. . . . . . 7 wff ( f ` ( 1r ` r ) ) = ( 1r ` s )
19		vx	. . . . . . . . . . . . . 14 setvar x
20	19	cv 1352	. . . . . . . . . . . . 13 class x
21		vy	. . . . . . . . . . . . . 14 setvar y
22	21	cv 1352	. . . . . . . . . . . . 13 class y
23		cplusg 12536	. . . . . . . . . . . . . 14 class +g
24	6, 23	cfv 5217	. . . . . . . . . . . . 13 class ( +g ` r )
25	20, 22, 24	co 5875	. . . . . . . . . . . 12 class ( x ( +g ` r ) y )
26	25, 15	cfv 5217	. . . . . . . . . . 11 class ( f ` ( x ( +g ` r ) y ) )
27	20, 15	cfv 5217	. . . . . . . . . . . 12 class ( f ` x )
28	22, 15	cfv 5217	. . . . . . . . . . . 12 class ( f ` y )
29	10, 23	cfv 5217	. . . . . . . . . . . 12 class ( +g ` s )
30	27, 28, 29	co 5875	. . . . . . . . . . 11 class ( ( f ` x ) ( +g ` s ) ( f ` y ) )
31	26, 30	wceq 1353	. . . . . . . . . 10 wff ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) )
32		cmulr 12537	. . . . . . . . . . . . . 14 class .r
33	6, 32	cfv 5217	. . . . . . . . . . . . 13 class ( .r ` r )
34	20, 22, 33	co 5875	. . . . . . . . . . . 12 class ( x ( .r ` r ) y )
35	34, 15	cfv 5217	. . . . . . . . . . 11 class ( f ` ( x ( .r ` r ) y ) )
36	10, 32	cfv 5217	. . . . . . . . . . . 12 class ( .r ` s )
37	27, 28, 36	co 5875	. . . . . . . . . . 11 class ( ( f ` x ) ( .r ` s ) ( f ` y ) )
38	35, 37	wceq 1353	. . . . . . . . . 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 1352	. . . . . . . . 9 class v
41	39, 21, 40	wral 2455	. . . . . . . 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 2455	. . . . . . 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 1352	. . . . . . 7 class w
45		cmap 6648	. . . . . . 7 class ^m
46	44, 40, 45	co 5875	. . . . . 6 class ( w ^m v )
47	43, 14, 46	crab 2459	. . . . 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 3058	. . . 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 3058	. . 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 5877	. 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 1353	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: (None)