Theorem isrhmd

Description: Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	isrhmd.b	$$⊢B={\mathrm{Base}}_R$$
	isrhmd.o	$$⊢\underset{\dot{}}{1}=1_R$$
	isrhmd.n	$$⊢N=1_S$$
	isrhmd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isrhmd.u	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	isrhmd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	isrhmd.s	$$⊢\phi \to S\in \mathrm{Ring}$$
	isrhmd.ho	$$⊢\phi \to F\left(\underset{\dot{}}{1}\right)=N$$
	isrhmd.ht	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)$$
	isrhmd.c	$$⊢C={\mathrm{Base}}_S$$
	isrhmd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	isrhmd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
	isrhmd.f	$$⊢\phi \to F:B⟶C$$
	isrhmd.hp	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
Assertion	isrhmd	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrhmd.b	$$⊢B={\mathrm{Base}}_R$$
2		isrhmd.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		isrhmd.n	$$⊢N=1_S$$
4		isrhmd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		isrhmd.u	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
6		isrhmd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		isrhmd.s	$$⊢\phi \to S\in \mathrm{Ring}$$
8		isrhmd.ho	$$⊢\phi \to F\left(\underset{\dot{}}{1}\right)=N$$
9		isrhmd.ht	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)$$
10		isrhmd.c	$$⊢C={\mathrm{Base}}_S$$
11		isrhmd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
12		isrhmd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
13		isrhmd.f	$$⊢\phi \to F:B⟶C$$
14		isrhmd.hp	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
15		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
16	6 15	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
17		ringgrp	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Grp}$$
18	7 17	syl	$$⊢\phi \to S\in \mathrm{Grp}$$
19	1 10 11 12 16 18 13 14	isghmd	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
20	1 2 3 4 5 6 7 8 9 19	isrhm2d	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$