Theorem isrnghm2d

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 ) ) )
	isrnghm2d.f	|- ( ph -> F e. ( R GrpHom S ) )
Assertion	isrnghm2d	|- ( ph -> F e. ( R RngHomo 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		isrnghm2d.f	|- ( ph -> F e. ( R GrpHom S ) )
8	4 5	jca	|- ( ph -> ( R e. Rng /\ S e. Rng ) )
9	6	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
10	7 9	jca	|- ( ph -> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) )
11	1 2 3	isrnghm	|- ( F e. ( R RngHomo S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) )
12	8 10 11	sylanbrc	|- ( ph -> F e. ( R RngHomo S ) )