isrhmd

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

	Ref	Expression
Hypotheses	isrhmd.b	$⊢ B = {Base}_{R}$
	isrhmd.o	$⊢ \underset{˙}{1} = 1_{R}$
	isrhmd.n	$⊢ N = 1_{S}$
	isrhmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isrhmd.u	$⊢ \underset{˙}{\times} = \cdot_{S}$
	isrhmd.r	$⊢ φ \to R \in Ring$
	isrhmd.s	$⊢ φ \to S \in Ring$
	isrhmd.ho	$⊢ φ \to F (\underset{˙}{1}) = N$
	isrhmd.ht	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
	isrhmd.c	$⊢ C = {Base}_{S}$
	isrhmd.p	$⊢ \underset{˙}{+} = +_{R}$
	isrhmd.q	$⊢ \underset{˙}{⨣} = +_{S}$
	isrhmd.f	$⊢ φ \to F : B ⟶ C$
	isrhmd.hp	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
Assertion	isrhmd	$⊢ φ \to F \in (R RingHom S)$

Step	Hyp	Ref	Expression
1		isrhmd.b	$⊢ B = {Base}_{R}$
2		isrhmd.o	$⊢ \underset{˙}{1} = 1_{R}$
3		isrhmd.n	$⊢ N = 1_{S}$
4		isrhmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		isrhmd.u	$⊢ \underset{˙}{\times} = \cdot_{S}$
6		isrhmd.r	$⊢ φ \to R \in Ring$
7		isrhmd.s	$⊢ φ \to S \in Ring$
8		isrhmd.ho	$⊢ φ \to F (\underset{˙}{1}) = N$
9		isrhmd.ht	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
10		isrhmd.c	$⊢ C = {Base}_{S}$
11		isrhmd.p	$⊢ \underset{˙}{+} = +_{R}$
12		isrhmd.q	$⊢ \underset{˙}{⨣} = +_{S}$
13		isrhmd.f	$⊢ φ \to F : B ⟶ C$
14		isrhmd.hp	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
15		ringgrp	$⊢ R \in Ring \to R \in Grp$
16	6 15	syl	$⊢ φ \to R \in Grp$
17		ringgrp	$⊢ S \in Ring \to S \in Grp$
18	7 17	syl	$⊢ φ \to S \in Grp$
19	1 10 11 12 16 18 13 14	isghmd	$⊢ φ \to F \in (R GrpHom S)$
20	1 2 3 4 5 6 7 8 9 19	isrhm2d	$⊢ φ \to F \in (R RingHom S)$

Metamath Proof Explorer