Theorem zrhpropd

Description: The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	zrhpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	zrhpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	zrhpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	zrhpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	zrhpropd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrhpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		zrhpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		zrhpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4		zrhpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
5		eqidd	$$⊢\phi \to {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
6		eqidd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge y\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)\to x{+}_{{\mathbb{Z}}_{\mathrm{ring}}}y=x{+}_{{\mathbb{Z}}_{\mathrm{ring}}}y$$
7		eqidd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\wedge y\in {\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}\right)\right)\to x{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}y=x{\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}y$$
8	5 1 5 2 6 3 7 4	rhmpropd	$$⊢\phi \to {\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K={\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}L$$
9	8	unieqd	$$⊢\phi \to \bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}L\right)$$
10		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(K\right)$$
11	10	zrhval	$$⊢\mathrm{\mathbb{Z}RHom}\left(K\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}K\right)$$
12		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(L\right)=\mathrm{\mathbb{Z}RHom}\left(L\right)$$
13	12	zrhval	$$⊢\mathrm{\mathbb{Z}RHom}\left(L\right)=\bigcup \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}L\right)$$
14	9 11 13	3eqtr4g	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(K\right)=\mathrm{\mathbb{Z}RHom}\left(L\right)$$