rnghmval

Description: The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020)

	Ref	Expression
Hypotheses	isrnghm.b	\|- B = ( Base ` R )
	isrnghm.t	\|- .x. = ( .r ` R )
	isrnghm.m	\|- .* = ( .r ` S )
	rnghmval.c	\|- C = ( Base ` S )
	rnghmval.p	\|- .+ = ( +g ` R )
	rnghmval.a	\|- .+b = ( +g ` S )
Assertion	rnghmval	\|- ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		isrnghm.b	\|- B = ( Base ` R )
2		isrnghm.t	\|- .x. = ( .r ` R )
3		isrnghm.m	\|- .* = ( .r ` S )
4		rnghmval.c	\|- C = ( Base ` S )
5		rnghmval.p	\|- .+ = ( +g ` R )
6		rnghmval.a	\|- .+b = ( +g ` S )
7		df-rnghm	\|- RngHom = ( 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 ) ) ) } )
8	7	a1i	\|- ( ( R e. Rng /\ S e. Rng ) -> RngHom = ( 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 ) ) ) } ) )
9		fveq2	\|- ( r = R -> ( Base ` r ) = ( Base ` R ) )
10	9 1	eqtr4di	\|- ( r = R -> ( Base ` r ) = B )
11	10	csbeq1d	\|- ( r = R -> [_ ( 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 ) ) ) } = [_ B / 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 ) ) ) } )
12		fveq2	\|- ( s = S -> ( Base ` s ) = ( Base ` S ) )
13	12 4	eqtr4di	\|- ( s = S -> ( Base ` s ) = C )
14	13	csbeq1d	\|- ( s = S -> [_ ( 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 ) ) ) } = [_ C / 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 ) ) ) } )
15	14	csbeq2dv	\|- ( s = S -> [_ B / 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
16	11 15	sylan9eq	\|- ( ( r = R /\ s = S ) -> [_ ( 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
17	16	adantl	\|- ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ ( 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
18	1	fvexi	\|- B e. _V
19	4	fvexi	\|- C e. _V
20		oveq12	\|- ( ( w = C /\ v = B ) -> ( w ^m v ) = ( C ^m B ) )
21	20	ancoms	\|- ( ( v = B /\ w = C ) -> ( w ^m v ) = ( C ^m B ) )
22		raleq	\|- ( v = B -> ( 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 ) ) ) <-> A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
23	22	raleqbi1dv	\|- ( v = B -> ( 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 ) ) ) <-> A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
24	23	adantr	\|- ( ( v = B /\ w = C ) -> ( 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 ) ) ) <-> A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
25	21 24	rabeqbidv	\|- ( ( v = B /\ w = C ) -> { 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 ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )
26	18 19 25	csbie2	\|- [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) }
27		fveq2	\|- ( r = R -> ( +g ` r ) = ( +g ` R ) )
28	27 5	eqtr4di	\|- ( r = R -> ( +g ` r ) = .+ )
29	28	oveqdr	\|- ( ( r = R /\ s = S ) -> ( x ( +g ` r ) y ) = ( x .+ y ) )
30	29	fveq2d	\|- ( ( r = R /\ s = S ) -> ( f ` ( x ( +g ` r ) y ) ) = ( f ` ( x .+ y ) ) )
31		fveq2	\|- ( s = S -> ( +g ` s ) = ( +g ` S ) )
32	31 6	eqtr4di	\|- ( s = S -> ( +g ` s ) = .+b )
33	32	adantl	\|- ( ( r = R /\ s = S ) -> ( +g ` s ) = .+b )
34	33	oveqd	\|- ( ( r = R /\ s = S ) -> ( ( f ` x ) ( +g ` s ) ( f ` y ) ) = ( ( f ` x ) .+b ( f ` y ) ) )
35	30 34	eqeq12d	\|- ( ( r = R /\ s = S ) -> ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) <-> ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) ) )
36		fveq2	\|- ( r = R -> ( .r ` r ) = ( .r ` R ) )
37	36 2	eqtr4di	\|- ( r = R -> ( .r ` r ) = .x. )
38	37	oveqdr	\|- ( ( r = R /\ s = S ) -> ( x ( .r ` r ) y ) = ( x .x. y ) )
39	38	fveq2d	\|- ( ( r = R /\ s = S ) -> ( f ` ( x ( .r ` r ) y ) ) = ( f ` ( x .x. y ) ) )
40		fveq2	\|- ( s = S -> ( .r ` s ) = ( .r ` S ) )
41	40 3	eqtr4di	\|- ( s = S -> ( .r ` s ) = .* )
42	41	adantl	\|- ( ( r = R /\ s = S ) -> ( .r ` s ) = .* )
43	42	oveqd	\|- ( ( r = R /\ s = S ) -> ( ( f ` x ) ( .r ` s ) ( f ` y ) ) = ( ( f ` x ) .* ( f ` y ) ) )
44	39 43	eqeq12d	\|- ( ( r = R /\ s = S ) -> ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) )
45	35 44	anbi12d	\|- ( ( r = R /\ s = S ) -> ( ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) <-> ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) ) )
46	45	2ralbidv	\|- ( ( r = R /\ s = S ) -> ( A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) <-> A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) ) )
47	46	rabbidv	\|- ( ( r = R /\ s = S ) -> { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
48	26 47	eqtrid	\|- ( ( r = R /\ s = S ) -> [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
49	48	adantl	\|- ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
50	17 49	eqtrd	\|- ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ ( 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 ) ) ) } = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
51		simpl	\|- ( ( R e. Rng /\ S e. Rng ) -> R e. Rng )
52		simpr	\|- ( ( R e. Rng /\ S e. Rng ) -> S e. Rng )
53		ovex	\|- ( C ^m B ) e. _V
54	53	rabex	\|- { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } e. _V
55	54	a1i	\|- ( ( R e. Rng /\ S e. Rng ) -> { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } e. _V )
56	8 50 51 52 55	ovmpod	\|- ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = { f e. ( C ^m B ) \| A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )

Metamath Proof Explorer

Theorem rnghmval

Proof