Theorem isrnghmd

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

	Ref	Expression
Hypotheses	isrnghmd.b	|- B = ( Base ` R )
	isrnghmd.t	|- .x. = ( .r ` R )
	isrnghmd.u	|- .X. = ( .r ` S )
	isrnghmd.r	|- ( ph -> R e. Rng )
	isrnghmd.s	|- ( ph -> S e. Rng )
	isrnghmd.ht	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
	isrnghmd.c	|- C = ( Base ` S )
	isrnghmd.p	|- .+ = ( +g ` R )
	isrnghmd.q	|- .+^ = ( +g ` S )
	isrnghmd.f	|- ( ph -> F : B --> C )
	isrnghmd.hp	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
Assertion	isrnghmd	|- ( ph -> F e. ( R RngHom S ) )

Proof

Step	Hyp	Ref	Expression
1		isrnghmd.b	|- B = ( Base ` R )
2		isrnghmd.t	|- .x. = ( .r ` R )
3		isrnghmd.u	|- .X. = ( .r ` S )
4		isrnghmd.r	|- ( ph -> R e. Rng )
5		isrnghmd.s	|- ( ph -> S e. Rng )
6		isrnghmd.ht	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
7		isrnghmd.c	|- C = ( Base ` S )
8		isrnghmd.p	|- .+ = ( +g ` R )
9		isrnghmd.q	|- .+^ = ( +g ` S )
10		isrnghmd.f	|- ( ph -> F : B --> C )
11		isrnghmd.hp	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
12		rngabl	|- ( R e. Rng -> R e. Abel )
13		ablgrp	|- ( R e. Abel -> R e. Grp )
14	4 12 13	3syl	|- ( ph -> R e. Grp )
15		rngabl	|- ( S e. Rng -> S e. Abel )
16		ablgrp	|- ( S e. Abel -> S e. Grp )
17	5 15 16	3syl	|- ( ph -> S e. Grp )
18	1 7 8 9 14 17 10 11	isghmd	|- ( ph -> F e. ( R GrpHom S ) )
19	1 2 3 4 5 6 18	isrnghm2d	|- ( ph -> F e. ( R RngHom S ) )