Theorem rhmval0

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by AV, 24-Jul-2026)

	Ref	Expression
Hypotheses	rhmval0.b	$$⊢B={\mathrm{Base}}_R$$
	rhmval0.c	$$⊢C={\mathrm{Base}}_S$$
	rhmval0.1	$$⊢\underset{\dot{}}{1}=1_R$$
	rhmval0.i	$$⊢N=1_S$$
	rhmval0.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rhmval0.n	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	rhmval0.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	rhmval0.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
Assertion	rhmval0	$$⊢\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\to R\mathrm{RingHom}S=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rhmval0.b	$$⊢B={\mathrm{Base}}_R$$
2		rhmval0.c	$$⊢C={\mathrm{Base}}_S$$
3		rhmval0.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		rhmval0.i	$$⊢N=1_S$$
5		rhmval0.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		rhmval0.n	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
7		rhmval0.p	$$⊢\underset{\dot{}}{+}={+}_R$$
8		rhmval0.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
9		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
10	9 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
11	10	adantr	$$⊢\left(r=R\wedge s=S\right)\to {\mathrm{Base}}_r=B$$
12		fveq2	$$⊢r=R\to 1_r=1_R$$
13	12 3	eqtr4di	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
14	13	fveq2d	$$⊢r=R\to f\left(1_r\right)=f\left(\underset{\dot{}}{1}\right)$$
15		fveq2	$$⊢s=S\to 1_s=1_S$$
16	15 4	eqtr4di	$$⊢s=S\to 1_s=N$$
17	14 16	eqeqan12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(1_r\right)=1_s\leftrightarrow f\left(\underset{\dot{}}{1}\right)=N\right)$$
18		fveq2	$$⊢r=R\to {+}_r={+}_R$$
19	18 7	eqtr4di	$$⊢r=R\to {+}_r=\underset{\dot{}}{+}$$
20	19	oveqd	$$⊢r=R\to x{+}_{r}y=x\underset{\dot{}}{+}y$$
21	20	fveq2d	$$⊢r=R\to f\left(x{+}_{r}y\right)=f\left(x\underset{\dot{}}{+}y\right)$$
22		fveq2	$$⊢s=S\to {+}_s={+}_S$$
23	22 8	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{⨣}$$
24	23	oveqd	$$⊢s=S\to f\left(x\right){+}_{s}f\left(y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)$$
25	21 24	eqeqan12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\leftrightarrow f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
26		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
27	26 5	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
28	27	oveqd	$$⊢r=R\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
29	28	fveq2d	$$⊢r=R\to f\left(x{\cdot }_{r}y\right)=f\left(x\underset{\dot{}}{·}y\right)$$
30		fveq2	$$⊢s=S\to {\cdot }_s={\cdot }_S$$
31	30 6	eqtr4di	$$⊢s=S\to {\cdot }_s=\underset{\dot{}}{\times }$$
32	31	oveqd	$$⊢s=S\to f\left(x\right){\cdot }_{s}f\left(y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)$$
33	29 32	eqeqan12d	$$⊢\left(r=R\wedge s=S\right)\to \left(f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\leftrightarrow f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)$$
34	25 33	anbi12d	$$⊢\left(r=R\wedge s=S\right)\to \left(\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\leftrightarrow \left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
35	34	2ralbidv	$$⊢\left(r=R\wedge s=S\right)\to \left(\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\leftrightarrow \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
36	17 35	anbi12d	$$⊢\left(r=R\wedge s=S\right)\to \left(\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\leftrightarrow \left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right)$$
37	36	rabbidv	$$⊢\left(r=R\wedge s=S\right)\to \left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}=\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
38	37	csbeq2dv	$$⊢\left(r=R\wedge s=S\right)\to ⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}=⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
39	11 38	csbeq12dv	$$⊢\left(r=R\wedge s=S\right)\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}=⦋B/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
40		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
41	40 2	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=C$$
42	41	adantl	$$⊢\left(r=R\wedge s=S\right)\to {\mathrm{Base}}_s=C$$
43	42	csbeq1d	$$⊢\left(r=R\wedge s=S\right)\to ⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}=⦋C/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
44	43	csbeq2dv	$$⊢\left(r=R\wedge s=S\right)\to ⦋B/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}=⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
45	1	fvexi	$$⊢B\in \mathrm{V}$$
46	2	fvexi	$$⊢C\in \mathrm{V}$$
47		oveq12	$$⊢\left(w=C\wedge v=B\right)\to w^v=C^B$$
48	47	ancoms	$$⊢\left(v=B\wedge w=C\right)\to w^v=C^B$$
49		raleq	$$⊢v=B\to \left(\forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\leftrightarrow \forall x\in B\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
50		raleq	$$⊢v=B\to \left(\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\leftrightarrow \forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
51	50	ralbidv	$$⊢v=B\to \left(\forall x\in B\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
52	49 51	bitrd	$$⊢v=B\to \left(\forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
53	52	adantr	$$⊢\left(v=B\wedge w=C\right)\to \left(\forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)$$
54	53	anbi2d	$$⊢\left(v=B\wedge w=C\right)\to \left(\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\leftrightarrow \left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right)$$
55	48 54	rabeqbidv	$$⊢\left(v=B\wedge w=C\right)\to \left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
56	45 46 55	csbie2	$$⊢⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
57	56	a1i	$$⊢\left(r=R\wedge s=S\right)\to ⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in v\forall y\in v\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
58	39 44 57	3eqtrd	$$⊢\left(r=R\wedge s=S\right)\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$
59		df-rhm	$$⊢\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right)\right\}\right)$$
60		ovex	$$⊢C^B\in \mathrm{V}$$
61	60	rabex	$$⊢\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}\in \mathrm{V}$$
62	58 59 61	ovmpoa	$$⊢\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\to R\mathrm{RingHom}S=\left\{f\in \left(C^B\right)|\left(f\left(\underset{\dot{}}{1}\right)=N\wedge \forall x\in B\forall y\in B\left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\wedge f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\right)\right)\right\}$$