Theorem isrhm0

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010) (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	isrhm0	$$⊢\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\to \left(F\in \left(R\mathrm{RingHom}S\right)\leftrightarrow \left(F:B⟶C\wedge 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	1 2 3 4 5 6 7 8	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\}$$
10	9	eleq2d	$$⊢\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\to \left(F\in \left(R\mathrm{RingHom}S\right)\leftrightarrow F\in \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\}\right)$$
11	2	fvexi	$$⊢C\in \mathrm{V}$$
12	1	fvexi	$$⊢B\in \mathrm{V}$$
13	11 12	elmap	$$⊢F\in \left(C^B\right)\leftrightarrow F:B⟶C$$
14	13	anbi1i	$$⊢\left(F\in \left(C^B\right)\wedge \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)\leftrightarrow \left(F:B⟶C\wedge \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)$$
15		fveq1	$$⊢f=F\to f\left(\underset{\dot{}}{1}\right)=F\left(\underset{\dot{}}{1}\right)$$
16	15	eqeq1d	$$⊢f=F\to \left(f\left(\underset{\dot{}}{1}\right)=N\leftrightarrow F\left(\underset{\dot{}}{1}\right)=N\right)$$
17		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{+}y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
18		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
19		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
20	18 19	oveq12d	$$⊢f=F\to f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
21	17 20	eqeq12d	$$⊢f=F\to \left(f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\leftrightarrow F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\right)$$
22		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{·}y\right)=F\left(x\underset{\dot{}}{·}y\right)$$
23	18 19	oveq12d	$$⊢f=F\to f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)$$
24	22 23	eqeq12d	$$⊢f=F\to \left(f\left(x\underset{\dot{}}{·}y\right)=f\left(x\right)\underset{\dot{}}{\times }f\left(y\right)\leftrightarrow F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\right)$$
25	21 24	anbi12d	$$⊢f=F\to \left(\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 \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)$$
26	25	2ralbidv	$$⊢f=F\to \left(\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)\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)$$
27	16 26	anbi12d	$$⊢f=F\to \left(\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)\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)$$
28	27	elrab	$$⊢F\in \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\}\leftrightarrow \left(F\in \left(C^B\right)\wedge \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)$$
29		3anass	$$⊢\left(F:B⟶C\wedge 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)\leftrightarrow \left(F:B⟶C\wedge \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)$$
30	14 28 29	3bitr4i	$$⊢F\in \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\}\leftrightarrow \left(F:B⟶C\wedge 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)$$
31	10 30	bitrdi	$$⊢\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\to \left(F\in \left(R\mathrm{RingHom}S\right)\leftrightarrow \left(F:B⟶C\wedge 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)$$