isrnghmmul

Description: A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020)

	Ref	Expression
Hypotheses	isrnghmmul.m	$⊢ M = {mulGrp}_{R}$
	isrnghmmul.n	$⊢ N = {mulGrp}_{S}$
Assertion	isrnghmmul	$⊢ F \in (R RngHom S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in (M MgmHom N)))$

Proof

Step	Hyp	Ref	Expression
1		isrnghmmul.m	$⊢ M = {mulGrp}_{R}$
2		isrnghmmul.n	$⊢ N = {mulGrp}_{S}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		eqid	$⊢ \cdot_{S} = \cdot_{S}$
6	3 4 5	isrnghm	$⊢ F \in (R RngHom S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)))$
7	1	rngmgp	$⊢ R \in Rng \to M \in Smgrp$
8		sgrpmgm	$⊢ M \in Smgrp \to M \in Mgm$
9	7 8	syl	$⊢ R \in Rng \to M \in Mgm$
10	2	rngmgp	$⊢ S \in Rng \to N \in Smgrp$
11		sgrpmgm	$⊢ N \in Smgrp \to N \in Mgm$
12	10 11	syl	$⊢ S \in Rng \to N \in Mgm$
13	9 12	anim12i	$⊢ (R \in Rng \land S \in Rng) \to (M \in Mgm \land N \in Mgm)$
14		eqid	$⊢ {Base}_{S} = {Base}_{S}$
15	3 14	ghmf	$⊢ F \in (R GrpHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
16	13 15	anim12i	$⊢ ((R \in Rng \land S \in Rng) \land F \in (R GrpHom S)) \to ((M \in Mgm \land N \in Mgm) \land F : {Base}_{R} ⟶ {Base}_{S})$
17	16	biantrurd	$⊢ ((R \in Rng \land S \in Rng) \land F \in (R GrpHom S)) \to (\forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y) \leftrightarrow (((M \in Mgm \land N \in Mgm) \land F : {Base}_{R} ⟶ {Base}_{S}) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)))$
18		anass	$⊢ (((M \in Mgm \land N \in Mgm) \land F : {Base}_{R} ⟶ {Base}_{S}) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)) \leftrightarrow ((M \in Mgm \land N \in Mgm) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)))$
19	17 18	bitrdi	$⊢ ((R \in Rng \land S \in Rng) \land F \in (R GrpHom S)) \to (\forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y) \leftrightarrow ((M \in Mgm \land N \in Mgm) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y))))$
20	1 3	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
21	2 14	mgpbas	$⊢ {Base}_{S} = {Base}_{N}$
22	1 4	mgpplusg	$⊢ \cdot_{R} = +_{M}$
23	2 5	mgpplusg	$⊢ \cdot_{S} = +_{N}$
24	20 21 22 23	ismgmhm	$⊢ F \in (M MgmHom N) \leftrightarrow ((M \in Mgm \land N \in Mgm) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)))$
25	19 24	bitr4di	$⊢ ((R \in Rng \land S \in Rng) \land F \in (R GrpHom S)) \to (\forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y) \leftrightarrow F \in (M MgmHom N))$
26	25	pm5.32da	$⊢ (R \in Rng \land S \in Rng) \to ((F \in (R GrpHom S) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)) \leftrightarrow (F \in (R GrpHom S) \land F \in (M MgmHom N)))$
27	26	pm5.32i	$⊢ ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y))) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in (M MgmHom N)))$
28	6 27	bitri	$⊢ F \in (R RngHom S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in (M MgmHom N)))$

Metamath Proof Explorer

Theorem isrnghmmul

Proof