Theorem isrhmd

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

	Ref	Expression
Hypotheses	isrhmd.b	|- B = ( Base ` R )
	isrhmd.o	|- .1. = ( 1r ` R )
	isrhmd.n	|- N = ( 1r ` S )
	isrhmd.t	|- .x. = ( .r ` R )
	isrhmd.u	|- .X. = ( .r ` S )
	isrhmd.r	|- ( ph -> R e. Ring )
	isrhmd.s	|- ( ph -> S e. Ring )
	isrhmd.ho	|- ( ph -> ( F ` .1. ) = N )
	isrhmd.ht	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
	isrhmd.c	|- C = ( Base ` S )
	isrhmd.p	|- .+ = ( +g ` R )
	isrhmd.q	|- .+^ = ( +g ` S )
	isrhmd.f	|- ( ph -> F : B --> C )
	isrhmd.hp	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
Assertion	isrhmd	|- ( ph -> F e. ( R RingHom S ) )

Proof

Step	Hyp	Ref	Expression
1		isrhmd.b	|- B = ( Base ` R )
2		isrhmd.o	|- .1. = ( 1r ` R )
3		isrhmd.n	|- N = ( 1r ` S )
4		isrhmd.t	|- .x. = ( .r ` R )
5		isrhmd.u	|- .X. = ( .r ` S )
6		isrhmd.r	|- ( ph -> R e. Ring )
7		isrhmd.s	|- ( ph -> S e. Ring )
8		isrhmd.ho	|- ( ph -> ( F ` .1. ) = N )
9		isrhmd.ht	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
10		isrhmd.c	|- C = ( Base ` S )
11		isrhmd.p	|- .+ = ( +g ` R )
12		isrhmd.q	|- .+^ = ( +g ` S )
13		isrhmd.f	|- ( ph -> F : B --> C )
14		isrhmd.hp	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
15		ringgrp	|- ( R e. Ring -> R e. Grp )
16	6 15	syl	|- ( ph -> R e. Grp )
17		ringgrp	|- ( S e. Ring -> S e. Grp )
18	7 17	syl	|- ( ph -> S e. Grp )
19	1 10 11 12 16 18 13 14	isghmd	|- ( ph -> F e. ( R GrpHom S ) )
20	1 2 3 4 5 6 7 8 9 19	isrhm2d	|- ( ph -> F e. ( R RingHom S ) )