Theorem rhmpropd

Description: Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	rhmpropd.a	$$⊢\phi \to B={\mathrm{Base}}_J$$
	rhmpropd.b	$$⊢\phi \to C={\mathrm{Base}}_K$$
	rhmpropd.c	$$⊢\phi \to B={\mathrm{Base}}_L$$
	rhmpropd.d	$$⊢\phi \to C={\mathrm{Base}}_M$$
	rhmpropd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{J}y=x{+}_{L}y$$
	rhmpropd.f	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{+}_{K}y=x{+}_{M}y$$
	rhmpropd.g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{J}y=x{\cdot }_{L}y$$
	rhmpropd.h	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{M}y$$
Assertion	rhmpropd	$$⊢\phi \to J\mathrm{RingHom}K=L\mathrm{RingHom}M$$

Proof

Step	Hyp	Ref	Expression
1		rhmpropd.a	$$⊢\phi \to B={\mathrm{Base}}_J$$
2		rhmpropd.b	$$⊢\phi \to C={\mathrm{Base}}_K$$
3		rhmpropd.c	$$⊢\phi \to B={\mathrm{Base}}_L$$
4		rhmpropd.d	$$⊢\phi \to C={\mathrm{Base}}_M$$
5		rhmpropd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{J}y=x{+}_{L}y$$
6		rhmpropd.f	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{+}_{K}y=x{+}_{M}y$$
7		rhmpropd.g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{J}y=x{\cdot }_{L}y$$
8		rhmpropd.h	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{M}y$$
9	1 3 5 7	ringpropd	$$⊢\phi \to \left(J\in \mathrm{Ring}\leftrightarrow L\in \mathrm{Ring}\right)$$
10	2 4 6 8	ringpropd	$$⊢\phi \to \left(K\in \mathrm{Ring}\leftrightarrow M\in \mathrm{Ring}\right)$$
11	9 10	anbi12d	$$⊢\phi \to \left(\left(J\in \mathrm{Ring}\wedge K\in \mathrm{Ring}\right)\leftrightarrow \left(L\in \mathrm{Ring}\wedge M\in \mathrm{Ring}\right)\right)$$
12	1 2 3 4 5 6	ghmpropd	$$⊢\phi \to J\mathrm{GrpHom}K=L\mathrm{GrpHom}M$$
13	12	eleq2d	$$⊢\phi \to \left(f\in \left(J\mathrm{GrpHom}K\right)\leftrightarrow f\in \left(L\mathrm{GrpHom}M\right)\right)$$
14		eqid	$$⊢{\mathrm{mulGrp}}_J={\mathrm{mulGrp}}_J$$
15		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
16	14 15	mgpbas	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_{{\mathrm{mulGrp}}_J}$$
17	1 16	syl6eq	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_J}$$
18		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
19		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
20	18 19	mgpbas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
21	2 20	syl6eq	$$⊢\phi \to C={\mathrm{Base}}_{{\mathrm{mulGrp}}_K}$$
22		eqid	$$⊢{\mathrm{mulGrp}}_L={\mathrm{mulGrp}}_L$$
23		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
24	22 23	mgpbas	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
25	3 24	syl6eq	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{mulGrp}}_L}$$
26		eqid	$$⊢{\mathrm{mulGrp}}_M={\mathrm{mulGrp}}_M$$
27		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
28	26 27	mgpbas	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{{\mathrm{mulGrp}}_M}$$
29	4 28	syl6eq	$$⊢\phi \to C={\mathrm{Base}}_{{\mathrm{mulGrp}}_M}$$
30		eqid	$$⊢{\cdot }_J={\cdot }_J$$
31	14 30	mgpplusg	$$⊢{\cdot }_J={+}_{{\mathrm{mulGrp}}_J}$$
32	31	oveqi	$$⊢x{\cdot }_{J}y=x{+}_{{\mathrm{mulGrp}}_J}y$$
33		eqid	$$⊢{\cdot }_L={\cdot }_L$$
34	22 33	mgpplusg	$$⊢{\cdot }_L={+}_{{\mathrm{mulGrp}}_L}$$
35	34	oveqi	$$⊢x{\cdot }_{L}y=x{+}_{{\mathrm{mulGrp}}_L}y$$
36	7 32 35	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{{\mathrm{mulGrp}}_J}y=x{+}_{{\mathrm{mulGrp}}_L}y$$
37		eqid	$$⊢{\cdot }_K={\cdot }_K$$
38	18 37	mgpplusg	$$⊢{\cdot }_K={+}_{{\mathrm{mulGrp}}_K}$$
39	38	oveqi	$$⊢x{\cdot }_{K}y=x{+}_{{\mathrm{mulGrp}}_K}y$$
40		eqid	$$⊢{\cdot }_M={\cdot }_M$$
41	26 40	mgpplusg	$$⊢{\cdot }_M={+}_{{\mathrm{mulGrp}}_M}$$
42	41	oveqi	$$⊢x{\cdot }_{M}y=x{+}_{{\mathrm{mulGrp}}_M}y$$
43	8 39 42	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{+}_{{\mathrm{mulGrp}}_K}y=x{+}_{{\mathrm{mulGrp}}_M}y$$
44	17 21 25 29 36 43	mhmpropd	$$⊢\phi \to {\mathrm{mulGrp}}_J\mathrm{MndHom}{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_L\mathrm{MndHom}{\mathrm{mulGrp}}_M$$
45	44	eleq2d	$$⊢\phi \to \left(f\in \left({\mathrm{mulGrp}}_J\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)\leftrightarrow f\in \left({\mathrm{mulGrp}}_L\mathrm{MndHom}{\mathrm{mulGrp}}_M\right)\right)$$
46	13 45	anbi12d	$$⊢\phi \to \left(\left(f\in \left(J\mathrm{GrpHom}K\right)\wedge f\in \left({\mathrm{mulGrp}}_J\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)\right)\leftrightarrow \left(f\in \left(L\mathrm{GrpHom}M\right)\wedge f\in \left({\mathrm{mulGrp}}_L\mathrm{MndHom}{\mathrm{mulGrp}}_M\right)\right)\right)$$
47	11 46	anbi12d	$$⊢\phi \to \left(\left(\left(J\in \mathrm{Ring}\wedge K\in \mathrm{Ring}\right)\wedge \left(f\in \left(J\mathrm{GrpHom}K\right)\wedge f\in \left({\mathrm{mulGrp}}_J\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)\right)\right)\leftrightarrow \left(\left(L\in \mathrm{Ring}\wedge M\in \mathrm{Ring}\right)\wedge \left(f\in \left(L\mathrm{GrpHom}M\right)\wedge f\in \left({\mathrm{mulGrp}}_L\mathrm{MndHom}{\mathrm{mulGrp}}_M\right)\right)\right)\right)$$
48	14 18	isrhm	$$⊢f\in \left(J\mathrm{RingHom}K\right)\leftrightarrow \left(\left(J\in \mathrm{Ring}\wedge K\in \mathrm{Ring}\right)\wedge \left(f\in \left(J\mathrm{GrpHom}K\right)\wedge f\in \left({\mathrm{mulGrp}}_J\mathrm{MndHom}{\mathrm{mulGrp}}_K\right)\right)\right)$$
49	22 26	isrhm	$$⊢f\in \left(L\mathrm{RingHom}M\right)\leftrightarrow \left(\left(L\in \mathrm{Ring}\wedge M\in \mathrm{Ring}\right)\wedge \left(f\in \left(L\mathrm{GrpHom}M\right)\wedge f\in \left({\mathrm{mulGrp}}_L\mathrm{MndHom}{\mathrm{mulGrp}}_M\right)\right)\right)$$
50	47 48 49	3bitr4g	$$⊢\phi \to \left(f\in \left(J\mathrm{RingHom}K\right)\leftrightarrow f\in \left(L\mathrm{RingHom}M\right)\right)$$
51	50	eqrdv	$$⊢\phi \to J\mathrm{RingHom}K=L\mathrm{RingHom}M$$