Theorem isrhm2d

Description: Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-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)$$
	isrhm2d.f	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
Assertion	isrhm2d	$$⊢\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		isrhm2d.f	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
11		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
12	11	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
13	6 12	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
14		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
15	14	ringmgp	$$⊢S\in \mathrm{Ring}\to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
16	7 15	syl	$$⊢\phi \to {\mathrm{mulGrp}}_S\in \mathrm{Mnd}$$
17		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
18	1 17	ghmf	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F:B⟶{\mathrm{Base}}_S$$
19	10 18	syl	$$⊢\phi \to F:B⟶{\mathrm{Base}}_S$$
20	9	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)$$
21	11 2	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
22	21	fveq2i	$$⊢F\left(\underset{\dot{}}{1}\right)=F\left(0_{{\mathrm{mulGrp}}_R}\right)$$
23	14 3	ringidval	$$⊢N=0_{{\mathrm{mulGrp}}_S}$$
24	8 22 23	3eqtr3g	$$⊢\phi \to F\left(0_{{\mathrm{mulGrp}}_R}\right)=0_{{\mathrm{mulGrp}}_S}$$
25	19 20 24	3jca	$$⊢\phi \to \left(F:B⟶{\mathrm{Base}}_S\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\wedge F\left(0_{{\mathrm{mulGrp}}_R}\right)=0_{{\mathrm{mulGrp}}_S}\right)$$
26	11 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
27	14 17	mgpbas	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_{{\mathrm{mulGrp}}_S}$$
28	11 4	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
29	14 5	mgpplusg	$$⊢\underset{\dot{}}{\times }={+}_{{\mathrm{mulGrp}}_S}$$
30		eqid	$$⊢0_{{\mathrm{mulGrp}}_R}=0_{{\mathrm{mulGrp}}_R}$$
31		eqid	$$⊢0_{{\mathrm{mulGrp}}_S}=0_{{\mathrm{mulGrp}}_S}$$
32	26 27 28 29 30 31	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:B⟶{\mathrm{Base}}_S\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{·}y\right)=F\left(x\right)\underset{\dot{}}{\times }F\left(y\right)\wedge F\left(0_{{\mathrm{mulGrp}}_R}\right)=0_{{\mathrm{mulGrp}}_S}\right)\right)$$
33	13 16 25 32	syl21anbrc	$$⊢\phi \to F\in \left({\mathrm{mulGrp}}_R\mathrm{MndHom}{\mathrm{mulGrp}}_S\right)$$
34	10 33	jca	$$⊢\phi \to \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge F\in \left({\mathrm{mulGrp}}_R\mathrm{MndHom}{\mathrm{mulGrp}}_S\right)\right)$$
35	11 14	isrhm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\leftrightarrow \left(\left(R\in \mathrm{Ring}\wedge S\in \mathrm{Ring}\right)\wedge \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge F\in \left({\mathrm{mulGrp}}_R\mathrm{MndHom}{\mathrm{mulGrp}}_S\right)\right)\right)$$
36	6 7 34 35	syl21anbrc	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$