Theorem 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={\mathrm{Base}}_R$$
	isrnghm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isrnghm.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_S$$
	rnghmval.c	$$⊢C={\mathrm{Base}}_S$$
	rnghmval.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	rnghmval.a	$$⊢\underset{\dot{}}{✚}={+}_S$$
Assertion	rnghmval	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to R\mathrm{RngHomo}S=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		isrnghm.b	$$⊢B={\mathrm{Base}}_R$$
2		isrnghm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		isrnghm.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_S$$
4		rnghmval.c	$$⊢C={\mathrm{Base}}_S$$
5		rnghmval.p	$$⊢\underset{\dot{}}{+}={+}_R$$
6		rnghmval.a	$$⊢\underset{\dot{}}{✚}={+}_S$$
7		df-rnghomo	$$⊢\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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)$$
8	7	a1i	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to \mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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)$$
9		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
10	9 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
11	10	csbeq1d	$$⊢r=R\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=⦋B/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}$$
12		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
13	12 4	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=C$$
14	13	csbeq1d	$$⊢s=S\to ⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}$$
15	14	csbeq2dv	$$⊢s=S\to ⦋B/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}$$
16	11 15	sylan9eq	$$⊢\left(r=R\wedge s=S\right)\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}$$
17	16	adantl	$$⊢\left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(r=R\wedge s=S\right)\right)\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}$$
18	1	fvexi	$$⊢B\in \mathrm{V}$$
19	4	fvexi	$$⊢C\in \mathrm{V}$$
20		oveq12	$$⊢\left(w=C\wedge v=B\right)\to w^v=C^B$$
21	20	ancoms	$$⊢\left(v=B\wedge w=C\right)\to w^v=C^B$$
22		raleq	$$⊢v=B\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 B\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)$$
23	22	raleqbi1dv	$$⊢v=B\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 B\forall y\in B\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)$$
24	23	adantr	$$⊢\left(v=B\wedge w=C\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 B\forall y\in B\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)$$
25	21 24	rabeqbidv	$$⊢\left(v=B\wedge w=C\right)\to \left\{f\in \left(w^v\right)|\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\}=\left\{f\in \left(C^B\right)|\forall x\in B\forall y\in B\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\}$$
26	18 19 25	csbie2	$$⊢⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}=\left\{f\in \left(C^B\right)|\forall x\in B\forall y\in B\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\}$$
27		fveq2	$$⊢r=R\to {+}_r={+}_R$$
28	27 5	eqtr4di	$$⊢r=R\to {+}_r=\underset{\dot{}}{+}$$
29	28	oveqdr	$$⊢\left(r=R\wedge s=S\right)\to x{+}_{r}y=x\underset{\dot{}}{+}y$$
30	29	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to f\left(x{+}_{r}y\right)=f\left(x\underset{\dot{}}{+}y\right)$$
31		fveq2	$$⊢s=S\to {+}_s={+}_S$$
32	31 6	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{✚}$$
33	32	adantl	$$⊢\left(r=R\wedge s=S\right)\to {+}_s=\underset{\dot{}}{✚}$$
34	33	oveqd	$$⊢\left(r=R\wedge s=S\right)\to f\left(x\right){+}_{s}f\left(y\right)=f\left(x\right)\underset{\dot{}}{✚}f\left(y\right)$$
35	30 34	eqeq12d	$$⊢\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)$$
36		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
37	36 2	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
38	37	oveqdr	$$⊢\left(r=R\wedge s=S\right)\to x{\cdot }_{r}y=x\underset{\dot{}}{·}y$$
39	38	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to f\left(x{\cdot }_{r}y\right)=f\left(x\underset{\dot{}}{·}y\right)$$
40		fveq2	$$⊢s=S\to {\cdot }_s={\cdot }_S$$
41	40 3	eqtr4di	$$⊢s=S\to {\cdot }_s=\underset{\dot{}}{\ast }$$
42	41	adantl	$$⊢\left(r=R\wedge s=S\right)\to {\cdot }_s=\underset{\dot{}}{\ast }$$
43	42	oveqd	$$⊢\left(r=R\wedge s=S\right)\to f\left(x\right){\cdot }_{s}f\left(y\right)=f\left(x\right)\underset{\dot{}}{\ast }f\left(y\right)$$
44	39 43	eqeq12d	$$⊢\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{}}{\ast }f\left(y\right)\right)$$
45	35 44	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{}}{\ast }f\left(y\right)\right)\right)$$
46	45	2ralbidv	$$⊢\left(r=R\wedge s=S\right)\to \left(\forall x\in B\forall y\in B\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 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{}}{\ast }f\left(y\right)\right)\right)$$
47	46	rabbidv	$$⊢\left(r=R\wedge s=S\right)\to \left\{f\in \left(C^B\right)|\forall x\in B\forall y\in B\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\}=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$
48	26 47	syl5eq	$$⊢\left(r=R\wedge s=S\right)\to ⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$
49	48	adantl	$$⊢\left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(r=R\wedge s=S\right)\right)\to ⦋B/v⦌⦋C/w⦌\left\{f\in \left(w^v\right)|\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\}=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$
50	17 49	eqtrd	$$⊢\left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(r=R\wedge s=S\right)\right)\to ⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\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\}=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$
51		simpl	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to R\in \mathrm{Rng}$$
52		simpr	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to S\in \mathrm{Rng}$$
53		ovex	$$⊢C^B\in \mathrm{V}$$
54	53	rabex	$$⊢\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}\in \mathrm{V}$$
55	54	a1i	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to \left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}\in \mathrm{V}$$
56	8 50 51 52 55	ovmpod	$$⊢\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\to R\mathrm{RngHomo}S=\left\{f\in \left(C^B\right)|\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{}}{\ast }f\left(y\right)\right)\right\}$$