Theorem dfrhm2

Description: The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	dfrhm2	$$⊢\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼\left(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		ancom	$$⊢\left(f\left(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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)\wedge f\left(1_r\right)=1_s\right)$$
3		r19.26-2	$$⊢\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)$$
4	3	anbi1i	$$⊢\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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)\wedge f\left(1_r\right)=1_s\right)\leftrightarrow \left(\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\wedge f\left(1_r\right)=1_s\right)$$
5		anass	$$⊢\left(\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\wedge f\left(1_r\right)=1_s\right)\leftrightarrow \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
6	2 4 5	3bitri	$$⊢\left(f\left(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
7	6	rabbii	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\right\}$$
8		fvex	$$⊢{\mathrm{Base}}_r\in \mathrm{V}$$
9		fvex	$$⊢{\mathrm{Base}}_s\in \mathrm{V}$$
10		oveq12	$$⊢\left(w={\mathrm{Base}}_s\wedge v={\mathrm{Base}}_r\right)\to w^v={{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}$$
11	10	ancoms	$$⊢\left(v={\mathrm{Base}}_r\wedge w={\mathrm{Base}}_s\right)\to w^v={{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}$$
12		raleq	$$⊢v={\mathrm{Base}}_r\to \left(\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 y\in {\mathrm{Base}}_r\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)$$
13	12	raleqbi1dv	$$⊢v={\mathrm{Base}}_r\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 {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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)$$
14	13	adantr	$$⊢\left(v={\mathrm{Base}}_r\wedge w={\mathrm{Base}}_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 {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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)$$
15	14	anbi2d	$$⊢\left(v={\mathrm{Base}}_r\wedge w={\mathrm{Base}}_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(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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)$$
16	11 15	rabeqbidv	$$⊢\left(v={\mathrm{Base}}_r\wedge w={\mathrm{Base}}_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({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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\}$$
17	8 9 16	csbie2	$$⊢⦋{\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({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(f\left(1_r\right)=1_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\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\}$$
18		inrab	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}\cap \left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}=\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\right\}$$
19	7 17 18	3eqtr4i	$$⊢⦋{\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({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}\cap \left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
20		ringgrp	$$⊢r\in \mathrm{Ring}\to r\in \mathrm{Grp}$$
21		ringgrp	$$⊢s\in \mathrm{Ring}\to s\in \mathrm{Grp}$$
22		eqid	$$⊢{\mathrm{Base}}_r={\mathrm{Base}}_r$$
23		eqid	$$⊢{\mathrm{Base}}_s={\mathrm{Base}}_s$$
24		eqid	$$⊢{+}_r={+}_r$$
25		eqid	$$⊢{+}_s={+}_s$$
26	22 23 24 25	isghm3	$$⊢\left(r\in \mathrm{Grp}\wedge s\in \mathrm{Grp}\right)\to \left(f\in \left(r\mathrm{GrpHom}s\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right)$$
27	20 21 26	syl2an	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to \left(f\in \left(r\mathrm{GrpHom}s\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right)$$
28	27	eqabdv	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to r\mathrm{GrpHom}s=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right\}$$
29		df-rab	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}=\left\{f|\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right\}$$
30	9 8	elmap	$$⊢f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\leftrightarrow f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s$$
31	30	anbi1i	$$⊢\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)$$
32	31	abbii	$$⊢\left\{f|\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right\}=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right\}$$
33	29 32	eqtri	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right)\right\}$$
34	28 33	eqtr4di	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to r\mathrm{GrpHom}s=\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}$$
35		eqid	$$⊢{\mathrm{mulGrp}}_r={\mathrm{mulGrp}}_r$$
36	35	ringmgp	$$⊢r\in \mathrm{Ring}\to {\mathrm{mulGrp}}_r\in \mathrm{Mnd}$$
37		eqid	$$⊢{\mathrm{mulGrp}}_s={\mathrm{mulGrp}}_s$$
38	37	ringmgp	$$⊢s\in \mathrm{Ring}\to {\mathrm{mulGrp}}_s\in \mathrm{Mnd}$$
39	35 22	mgpbas	$$⊢{\mathrm{Base}}_r={\mathrm{Base}}_{{\mathrm{mulGrp}}_r}$$
40	37 23	mgpbas	$$⊢{\mathrm{Base}}_s={\mathrm{Base}}_{{\mathrm{mulGrp}}_s}$$
41		eqid	$$⊢{\cdot }_r={\cdot }_r$$
42	35 41	mgpplusg	$$⊢{\cdot }_r={+}_{{\mathrm{mulGrp}}_r}$$
43		eqid	$$⊢{\cdot }_s={\cdot }_s$$
44	37 43	mgpplusg	$$⊢{\cdot }_s={+}_{{\mathrm{mulGrp}}_s}$$
45		eqid	$$⊢1_r=1_r$$
46	35 45	ringidval	$$⊢1_r=0_{{\mathrm{mulGrp}}_r}$$
47		eqid	$$⊢1_s=1_s$$
48	37 47	ringidval	$$⊢1_s=0_{{\mathrm{mulGrp}}_s}$$
49	39 40 42 44 46 48	ismhm	$$⊢f\in \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\leftrightarrow \left(\left({\mathrm{mulGrp}}_r\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_s\in \mathrm{Mnd}\right)\wedge \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
50	49	baib	$$⊢\left({\mathrm{mulGrp}}_r\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_s\in \mathrm{Mnd}\right)\to \left(f\in \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
51	36 38 50	syl2an	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to \left(f\in \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
52	51	eqabdv	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
53		df-rab	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}=\left\{f|\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\right\}$$
54	30	anbi1i	$$⊢\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
55		3anass	$$⊢\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)$$
56	54 55	bitr4i	$$⊢\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)$$
57	56	abbii	$$⊢\left\{f|\left(f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)\wedge \left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right)\right\}=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
58	53 57	eqtri	$$⊢\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}=\left\{f|\left(f:{\mathrm{Base}}_r⟶{\mathrm{Base}}_s\wedge \forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
59	52 58	eqtr4di	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s=\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
60	34 59	ineq12d	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\right)\to \left(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)=\left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\right\}\cap \left\{f\in \left({{\mathrm{Base}}_s}^{{\mathrm{Base}}_r}\right)|\left(\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_{r}f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\wedge f\left(1_r\right)=1_s\right)\right\}$$
61	19 60	eqtr4id	$$⊢\left(r\in \mathrm{Ring}\wedge s\in \mathrm{Ring}\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(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)$$
62	61	mpoeq3ia	$$⊢\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)=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼\left(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\right)$$
63	1 62	eqtri	$$⊢\mathrm{RingHom}=\left(r\in \mathrm{Ring},s\in \mathrm{Ring}⟼\left(r\mathrm{GrpHom}s\right)\cap \left({\mathrm{mulGrp}}_r\mathrm{MndHom}{\mathrm{mulGrp}}_s\right)\right)$$