Theorem isrnghmd

Description: Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020)

	Ref	Expression
Hypotheses	isrnghmd.b	$$⊢B={\mathrm{Base}}_R$$
	isrnghmd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	isrnghmd.u	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	isrnghmd.r	$$⊢\phi \to R\in \mathrm{Rng}$$
	isrnghmd.s	$$⊢\phi \to S\in \mathrm{Rng}$$
	isrnghmd.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)$$
	isrnghmd.c	$$⊢C={\mathrm{Base}}_S$$
	isrnghmd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	isrnghmd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
	isrnghmd.f	$$⊢\phi \to F:B⟶C$$
	isrnghmd.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	isrnghmd	$$⊢\phi \to F\in \left(R\mathrm{RngHomo}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrnghmd.b	$$⊢B={\mathrm{Base}}_R$$
2		isrnghmd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		isrnghmd.u	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
4		isrnghmd.r	$$⊢\phi \to R\in \mathrm{Rng}$$
5		isrnghmd.s	$$⊢\phi \to S\in \mathrm{Rng}$$
6		isrnghmd.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)$$
7		isrnghmd.c	$$⊢C={\mathrm{Base}}_S$$
8		isrnghmd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
9		isrnghmd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
10		isrnghmd.f	$$⊢\phi \to F:B⟶C$$
11		isrnghmd.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)$$
12		rngabl	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$
13		ablgrp	$$⊢R\in \mathrm{Abel}\to R\in \mathrm{Grp}$$
14	4 12 13	3syl	$$⊢\phi \to R\in \mathrm{Grp}$$
15		rngabl	$$⊢S\in \mathrm{Rng}\to S\in \mathrm{Abel}$$
16		ablgrp	$$⊢S\in \mathrm{Abel}\to S\in \mathrm{Grp}$$
17	5 15 16	3syl	$$⊢\phi \to S\in \mathrm{Grp}$$
18	1 7 8 9 14 17 10 11	isghmd	$$⊢\phi \to F\in \left(R\mathrm{GrpHom}S\right)$$
19	1 2 3 4 5 6 18	isrnghm2d	$$⊢\phi \to F\in \left(R\mathrm{RngHomo}S\right)$$