isrnghm2d

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)$
	isrnghm2d.f	$⊢ φ \to F \in (R GrpHom S)$
Assertion	isrnghm2d	$⊢ φ \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		isrnghm2d.f	$⊢ φ \to F \in (R GrpHom S)$
8	4 5	jca	$⊢ φ \to (R \in Rng \land S \in Rng)$
9	6	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)$
10	7 9	jca	$⊢ φ \to (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y))$
11	1 2 3	isrnghm	$⊢ F \in (R RngHom S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in B \forall y \in B F (x \underset{˙}{\cdot} y) = F (x) \underset{˙}{\times} F (y)))$
12	8 10 11	sylanbrc	$⊢ φ \to F \in (R RngHom S)$

Metamath Proof Explorer