isrnghmd

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

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

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

Metamath Proof Explorer