Definition df-rnghomo 41887

Description: Define the set of non-unital ring homomorphisms from r to s. (Contributed by AV, 20-Feb-2020.)

Assertion

Ref	Expression
df-rnghomo	|- RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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-rnghomo

Step	Hyp	Ref	Expression
1		crngh 41885	. 2 class RngHomo
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crng 41874	. . 3 class Rng
5		vv	. . . 4 setvar v
6	2	cv 1482	. . . . 5 class r
7		cbs 15857	. . . . 5 class Base
8	6, 7	cfv 5888	. . . 4 class ( Base ` r )
9		vw	. . . . 5 setvar w
10	3	cv 1482	. . . . . 6 class s
11	10, 7	cfv 5888	. . . . 5 class ( Base ` s )
12		vx	. . . . . . . . . . . . 13 setvar x
13	12	cv 1482	. . . . . . . . . . . 12 class x
14		vy	. . . . . . . . . . . . 13 setvar y
15	14	cv 1482	. . . . . . . . . . . 12 class y
16		cplusg 15941	. . . . . . . . . . . . 13 class +g
17	6, 16	cfv 5888	. . . . . . . . . . . 12 class ( +g ` r )
18	13, 15, 17	co 6650	. . . . . . . . . . 11 class ( x ( +g ` r ) y )
19		vf	. . . . . . . . . . . 12 setvar f
20	19	cv 1482	. . . . . . . . . . 11 class f
21	18, 20	cfv 5888	. . . . . . . . . 10 class ( f ` ( x ( +g ` r ) y ) )
22	13, 20	cfv 5888	. . . . . . . . . . 11 class ( f ` x )
23	15, 20	cfv 5888	. . . . . . . . . . 11 class ( f ` y )
24	10, 16	cfv 5888	. . . . . . . . . . 11 class ( +g ` s )
25	22, 23, 24	co 6650	. . . . . . . . . 10 class ( ( f ` x ) ( +g ` s ) ( f ` y ) )
26	21, 25	wceq 1483	. . . . . . . . 9 wff ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) )
27		cmulr 15942	. . . . . . . . . . . . 13 class .r
28	6, 27	cfv 5888	. . . . . . . . . . . 12 class ( .r ` r )
29	13, 15, 28	co 6650	. . . . . . . . . . 11 class ( x ( .r ` r ) y )
30	29, 20	cfv 5888	. . . . . . . . . 10 class ( f ` ( x ( .r ` r ) y ) )
31	10, 27	cfv 5888	. . . . . . . . . . 11 class ( .r ` s )
32	22, 23, 31	co 6650	. . . . . . . . . 10 class ( ( f ` x ) ( .r ` s ) ( f ` y ) )
33	30, 32	wceq 1483	. . . . . . . . 9 wff ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) )
34	26, 33	wa 384	. . . . . . . 8 wff ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
35	5	cv 1482	. . . . . . . 8 class v
36	34, 14, 35	wral 2912	. . . . . . 7 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 ) ) )
37	36, 12, 35	wral 2912	. . . . . 6 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 ) ) )
38	9	cv 1482	. . . . . . 7 class w
39		cmap 7857	. . . . . . 7 class ^m
40	38, 35, 39	co 6650	. . . . . 6 class ( w ^m v )
41	37, 19, 40	crab 2916	. . . . 5 class { f e. ( w ^m v ) | 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 ) ) ) }
42	9, 11, 41	csb 3533	. . . 4 class [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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	5, 8, 42	csb 3533	. . 3 class [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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	2, 3, 4, 4, 43	cmpt2 6652	. 2 class ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 ) ) ) } )
45	1, 44	wceq 1483	1 wff RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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:  rnghmrcl  41889  rnghmfn  41890  rnghmval  41891  rngchomrnghmresALTV  41996